The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

No, ``` (optionally suffixed by a language) is markdown syntax to 
indicate a code block (verbatim in latex terms)

Gaëtan Gilbert

On 05/02/2020 10:11, Jeremy Dawson wrote:
> 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