The Coq mailing list

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

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