I a am setting up a new project and I have the following
_CoqProject (copied from elsewhere):
-Q theories/ machines -arg -w -arg all theories/stlc.v
When I load emacs proof general does not start. I assume my file has an error or I am doing something silly, any ideas on figuring it out/ debugging?
Just copying such a file won't work, what have you updated, and what files do you have in your new project?
If you have
-Q theories/ machines in
foo/_CoqProject, then your sources must live under
foo/theories/. And your
_CoqProject only expects
foo/theories/stlc.v to exist.
To support more than one source file, you should also build them using
make — you can copy-paste
foo/Makefile from https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile, then invoke
make from a terminal in directory
If it's a new project, perhaps setting it up with dune might be a more modern way to do it?
I had the impression that existing projects had a tendency to convert to dune these days, but I may err.
When I load emacs proof general does not start.
What does that mean in specific terms? Is there an error? Is it actually installed? Does it work on other projects?
@Callan McGill in Coq-community, we recommend formulating
_CoqProject files like this, which should be compatible with ProofGeneral and others:
-Q theories machines -arg -w -arg +default theories/stlc.v
This would raise error on all warnings with coq_makefile+make, which I assume is what you want to do.
@Paolo Giarrusso I didn't _literally_ just copy the file, I changed the relevant names of the files (and managed to sort my issue now). Thank you for the info @Karl Palmskog , very helpful!
@Callan McGill sorry, I was only double-checking :sweat_smile:
Last updated: Sep 23 2023 at 06:01 UTC