The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

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
>      >
>