The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

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