The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Yes, CoqIDE does support _CoqProject as well. I don't know why I
didn't include it in my list.

The _CoqProject format is documented here:
https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-coq-makefile

Théo

Le jeu. 6 févr. 2020 à 15:09, Jeremy Dawson 
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> 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
> >      >
> >