The Coq mailing list

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

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