The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

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