Callan McGill (Jun 25 2022 at 04:44): Callan McGill (Jun 25 2022 at 04:44):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?
Paolo Giarrusso (Jun 25 2022 at 05:05):Just copying such a file won't work, what have you updated, and what files do you have in your new project?
Paolo Giarrusso (Jun 25 2022 at 05:07):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.
Paolo Giarrusso (Jun 25 2022 at 05:10):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 foo.
Julien Puydt (Jun 25 2022 at 05:57):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.
Gaëtan Gilbert (Jun 25 2022 at 06:36):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?
Karl Palmskog (Jun 25 2022 at 16:42):@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.
Callan McGill (Jun 25 2022 at 16:46):@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!
Paolo Giarrusso (Jun 25 2022 at 19:41):@Callan McGill sorry, I was only double-checking :sweat_smile:
Last updated: Sep 23 2023 at 06:01 UTC