The Coq mailing list

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

Hi,

Thanks - but this won't work because it would mean changing dd_fc.v
and all the files in that directory, which is part of other people's 
work as well

So I tried some alternatives like
-Q ../lnt/tense-logic-in-Coq/
or
-Q ../lnt/tense-logic-in-Coq/ .

All of these, including your suggested
-Q ../lnt/tense-logic-in-Coq/ TL

gave a bunch or warnings, eg

-Q ../lnt/tense-logic-in-Coq/ TL
gives
Warning: ../lnt/tense-logic-in-Coq/ (used in -R or -Q) is not a 
subdirectory of the current directory

Warning: no common logical root
Warning: in such case INSTALLDEFAULTROOT must be defined
Warning: the install-doc target is going to install files
Warning: in orphan_TL_Top

I don't understand any of these, except the first (and I don't know what 
I should do about that), and I can't find any explanation of these in 
the documentation.

What do they all mean?

Thanks

Jeremy


On 27/4/20 12:26 am, Gaëtan Gilbert wrote:
> Indeed -I is for ocaml files (for plugins)
>
> Gaëtan Gilbert
>
> On 26/04/2020 16:23, Dan Frumin wrote:
> > Hi Jeremy,
> >
> > I don't know why -I doesn't work, but I think using -Q does the trick 
> > (at least with my version of Coq): I replaced
> >
> >      -I ../lnt/tense-logic-in-Coq/
> >
> > with
> >      -Q ../lnt/tense-logic-in-Coq/ TL
> >
> > and then in dd_fc.v used `Require Import TL.genT`
> >
> >
> >
> > Best,
> > Dan
> >
> >
> > On 26-04-2020 16:09, Jeremy Dawson wrote:
> > > Hi,
> > >
> > > I've constructed a _CoqProject file as follows
> > >
> > > -I ../lnt/tense-logic-in-Coq/
> > > -I ../gen/
> > > ../lnt/tense-logic-in-Coq/gen.v
> > > ../lnt/tense-logic-in-Coq/genT.v
> > > ../lnt/tense-logic-in-Coq/List_lemmasT.v
> > > ../lnt/tense-logic-in-Coq/lntT.v
> > > ../lnt/tense-logic-in-Coq/swappedT.v
> > > ../lnt/tense-logic-in-Coq/ddT.v
> > > ../lnt/tense-logic-in-Coq/dd_fc.v
> > > ../lnt/tense-logic-in-Coq/lntacsT.v
> > > ../gen/rtcT.v
> > > ../gen/gstep.v
> > > ../gen/gentree.v
> > > gen_ext.v
> > > k4.v
> > > k4_exch.v
> > > k4_inv.v
> > > k4_ctr.v
> > > k4_ca.v
> > >
> > > I then run
> > >   make -f Makefile
> > > and get the following messages
> > > COQC ../lnt/tense-logic-in-Coq/dd_fc.v
> > > File "../lnt/tense-logic-in-Coq/dd_fc.v", line 12, characters 15-19:
> > > Error: Unable to locate library genT.
> > >
> > > (in fact the file
> > > ../lnt/tense-logic-in-Coq/genT.v
> > > exists)
> > >
> > > What do I need to put in the _CoqProject file to make this work?
> > >
> > > Thanks
> > >
> > > Jeremy