The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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/