The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

FTR this is documented in the "PRACTICAL TOOLS/ Coq Command" chapter of the
documentation:

https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html

and in  "PRACTICAL TOOLS/ Utilities":

https://coq.inria.fr/distrib/current/refman/practical-tools/utilities.html#utilities

P.

Le jeu. 6 févr. 2020 à 15:23, Ralf Jung 
<jung AT mpi-sws.org>
 a écrit :
>
> Hi Jeremy,
>
> if it helps to see an example, you can check out how we are using 
> _CoqProject in
> Iris:
>
> https://gitlab.mpi-sws.org/iris/iris/blob/master/_CoqProject
>
> In particular, note the "-Q theories iris". This means that the folder
> "theories" (relative to the _CoqProject file) becomes the Coq logical path 
> "iris".
>
> With this, you can just open any .v file in theories/* in CoqIDE, and all 
> the
> paths just work.  No need to pass any flags anywhere else.  (Well, this is 
> what
> happens with ProofGeneral, but I think CoqIDE is the same.)  And as already
> mentioned in this thread, the coq_makefile invocation is
>
> coq_makefile -f _CoqProject -o Makefile
>
> After that, running "make" will build all files listed in _CoqProject.
> (Notice that if you have a typo in that file list, really weird stuff can 
> happen
> -- that's a known bug: https://github.com/coq/coq/issues/9319.)
>
> Kind regards,
> Ralf
>
> On 06.02.20 15:09, Jeremy Dawson wrote:
> > Hi Theo,
> >
> > Thanks.  How about coqide (it's been mentioned to me previously, but
> > apparently it has the same options as coqtop, and it's documentation
> > within the reference manual doesn't seem to mention the _CoqProject file).
> >
> > And so far, I'm pretty much on my own regarding this _CoqProject file -
> > I can't find any documentation about how to set it up, when it is used,
> > and what it does.  Is there any such documentation?
> >
> > Thanks for the tip about echo $?
> >
> > Jeremy Dawson
> >
> >
> > On 6/2/20 7:48 pm, Théo Zimmermann wrote:
> >> Hi Jeremy,
> >>
> >> The _CoqProject file is supported by editors with Coq support (Emacs
> >> with PG, VsCode with VsCoq, etc.) and by coq_makefile. You are never
> >> supposed to run coqc nor coqtop directly by yourself. In particular,
> >> today coqtop is considered as just a debugging tool. If you do insist on
> >> using it standalone, you are pretty much on your own (and you'll have to
> >> figure out the flags you need to give it).
> >>
> >> Regarding how to make sure that a process such as make finished without
> >> error, you can print the exit code: echo $?
> >>
> >> Cheers,
> >> Théo
> >>
> >>
> >> Le jeu. 6 févr. 2020 à 01:59, Jeremy Dawson 
> >> <Jeremy.Dawson AT anu.edu.au
> >> <mailto:Jeremy.Dawson AT anu.edu.au>>
> >>  a écrit :
> >>
> >>     Well, make with the existing Makefile seems to make everything OK, I
> >>     suppose there is no way to tell for sure, but there is no apparent
> >>     error.
> >>
> >>     With a new _CoqProject file there are all sorts of errors, presumably
> >>     because the existing _CoqProject file has useful stuff in it.
> >>
> >>     But in any event, running coq (to be exact, coqtop) does not access
> >>     either _CoqProject or Makefile, so I can't see how your solution 
> >> should
> >>     work.  (Anyway, it doesn't).  Maybe I'm missing something here.  Can
> >>     you
> >>     explain how your solution should work.
> >>
> >>     Or can anyone refer me to where the documentation on this issue is,
> >>     if any?
> >>
> >>     Thanks
> >>
> >>     Jeremy
> >>
> >>
> >>     On 5/2/20 7:59 pm, Donald Leung wrote:
> >>      > Dear Jeremy,
> >>      >
> >>      > Try adding a `_CoqProject` file in the root directory of your Coq
> >>     development with the following contents:
> >>      >
> >>      > ```
> >>      > -Q ./tttt/TTT/ tttt.TTT
> >>      >
> >>      > ./tttt/TTT/ssss.v
> >>      > ./tttt/TTT/file2.v
> >>      > ./tttt/TTT/file3.v
> >>      > …
> >>      > ./tttt/TTT/filen.v
> >>      > ```
> >>      >
> >>      > where file2.v, file3.v, …, filen.v are the other vernacular files
> >>     in your Coq development that you would also like to compile. Then 
> >> run:
> >>      >
> >>      > ```bash
> >>      > $ coq_makefile -f _CoqProject -o Makefile
> >>      > ```
> >>      >
> >>      > in your command line and select `Compile > Make` in your CoqIDE
> >>     (or similar). Provided the build is successful, you should then be
> >>     able to step through the line:
> >>      >
> >>      > ```coq
> >>      >  From tttt.TTT Require Import ssss.
> >>      > ```
> >>      >
> >>      > in your CoqIDE (or similar) without any issues.
> >>      >
> >>      > Yours sincerely,
> >>      > Donald
> >>      >
> >>      >> Jeremy Dawson 
> >> <Jeremy.Dawson AT anu.edu.au
> >>     
> >> <mailto:Jeremy.Dawson AT anu.edu.au>>於2020年2月5日
> >>  15:00寫道：
> >>      >>
> >>      >> Hi,
> >>      >>
> >>      >> I'm trying to run a command which I was guessing should be
> >>      >>
> >>      >>  From tttt.TTT Require Import ssss.
> >>      >>
> >>      >> but I get the error
> >>      >>
> >>      >> Cannot find a physical path bound to logical path matching suffix
> >>      >> <> and prefix tttt.TTT.
> >>      >>
> >>      >> What does this mean?
> >>      >>
> >>      >> How do I use a file tttt/TTT/ssss.vo?
> >>      >>
> >>      >>
> >>      >> The documentation contains
> >>      >>   Variant From dirpath Require qualid
> >>      >> (in
> >>      >>
> >>     
> >> https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmdv.from-require)
> >>      >>
> >>      >> What should a dirpath look like, and where is it to be found in 
> >> the
> >>      >> documentation?  (Some of these syntax constructs seem to be
> >>     defined in
> >>      >>
> >>     
> >> https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html
> >>      >> but dirpath isn't - and none of them seem to be in the index)
> >>      >>
> >>      >> Thanks
> >>      >>
> >>      >> Jeremy
> >>      >
> >>
>
> --
> Website: https://people.mpi-sws.org/~jung/