The Coq mailing list

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

thanks Pierre - I'd found one of these but not the other

Jeremy

On 2/7/20 1:26 AM, Pierre Courtieu wrote:
> 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/