The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

You should remove all .vo generated before you had a makefile, so that
make rebuilds everything. `make clean` should probably do that. If it
still does not work you may have to point us to your real use case.

Best
Pierre

Le mer. 5 févr. 2020 à 09:03, Jeremy Dawson 
<Jeremy.Dawson AT anu.edu.au>
 a écrit :
>
> 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
> >      >      >
> >      >
> >