Stream: Coq users

Topic: _CoqProject issues


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jun 25 2022 at 19:41):

@Callan McGill sorry, I was only double-checking :sweat_smile:


Last updated: Feb 01 2023 at 11:04 UTC