The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

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