The Coq mailing list

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

Hi Donald,

I now take it that ``` is supposed to appear literally in the 
_CoqProject file, is that correct?

but typing
```bash
$ coq_makefile -f _CoqProject -o Makefile
```

literally into the command line seems to do nothing except do weird 
things to my terminal window.

Could you explain further?

Thanks

Jeremy

PS - it seems really weird that to Load or Require Import a file from a 
subdirectory requires remaking everything - is that really correct?


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
>