The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Did you order your _CoqProject properly? Did it build the files in the subdirectory first? (Do you have .vo files in the subdirectory corresponding to the .v files you want to import?)

R.

On Wed, Feb 5, 2020 at 8:43 AM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Thanks - that generates a Makefile, and make seems to work OK but then I get

 > From Cat Require Import sxxx.
 >                         ^^^^
Error:
Cannot find a physical path bound to logical path matching suffix
<> and prefix Cat.

Thanks,

Jeremy

On 5/2/20 6:34 pm, Ramkumar Ramachandra wrote:
> Try `coq_makefile -f _CoqProject -o Makefile`.
>
> R.
>
> On Wed, Feb 5, 2020 at 8:33 AM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au
> <mailto:Jeremy.Dawson AT anu.edu.au>> wrote:
>
>     Thanks - but coq_makefile doesn't generate a Makefile - it does
>     generate
>     a file called CoqMakefile.conf
>
>     Is coq_makefile documented?  It's not in the index (ie
>     https://coq.inria.fr/distrib/current/refman/genindex.html
>
>     Is this where I should be looking for documentation?  )
>
>     And the man page is hardly helpful
>
>     Thanks
>
>     Jeremy
>
>     On 5/2/20 6:14 pm, Ramkumar Ramachandra wrote:
>      > Hi Jeremy,
>      >
>      > You need to set up an `_CoqProject` like this:
>      >
>      > ```
>      > -Q category Cat
>      >
>      > category/cat.v
>      > category/ncat.v
>      > ```
>      >
>      > ... and run `coq_makefile` to generate a Makefile. Note that if
>     you can
>      > `make` the project, then Coq should work from Emacs just fine.
>      >
>      > In the example I've supplied, "category" is the subdirectory you
>     want to
>      > include, and you'd use `From Cat Require Import ...` to include a
>     file
>      > in it.
>      >
>      > R.
>      >
>      > On Wed, Feb 5, 2020 at 8:09 AM Jeremy Dawson
>     <Jeremy.Dawson AT anu.edu.au <mailto:Jeremy.Dawson AT anu.edu.au>
>      > <mailto:Jeremy.Dawson AT anu.edu.au
>     <mailto:Jeremy.Dawson AT anu.edu.au>>> wrote:
>      >
>      >     Hi,
>      >
>      >     The documentation at
>      >
>     https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmd.load
>      >     says
>      >
>      >           This command loads the file named ident.v, searching
>     successively
>      >     in each of the directories specified in the loadpath. (see
>     Section
>      >     Libraries and filesystem)
>      >     but when I go to that section it doesn't tell you how to set a
>      >     "loadpath" or how to view what it is (or even what it is, so I've
>      >     got to
>      >     guess it's as in other languages that I'm familiar with - and
>     that
>      >     somehow doesn't seem to fit the case)
>      >
>      >     So how do I load a file (eg, ttt/TTT/sss.v)
>      >
>      >     Thanks
>      >
>      >     Jeremy
>      >
>