The Coq mailing list

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

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