The Coq mailing list

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

Well, here is the _CoqProject file, just contains these two non-blank lines

-Q ttt/xxx Cat

ttt/xxx/sss.v

I don't think it built very much because the Makefile supplied to me 
with the files built a lot of stuff so I just got

make[1]: Nothing to be done for ...

but the directory ttt/xxx contains lots of .vo files

I would really like to know where to find information on this topic

Thanks

Jeremy




On 5/2/20 6:49 pm, Ramkumar Ramachandra wrote:
> 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
>  
> <mailto: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>
>      > 
> <mailto: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>>
>      >      > 
> <mailto: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
>      >      >
>      >
>