The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Don't use Add Loadpath, put the information in coproject instead
If you don't use a prefix then use -R

Gaëtan Gilbert

On 28/04/2020 15:43, Jeremy Dawson wrote:
> Hi Christian,
>
> Thanks.  But I don't use a prefix for Require Import.  For example here 
> are the relevant lines from one of the files.
>
> Add LoadPath "../gen".
> Add LoadPath "../lnt/tense-logic-in-Coq".
> Require Import gen genT ddT dd_fc.
> Require Import List_lemmasT.
> Require Import lntT.
> Require Import swappedT.
> Require Import lntacsT.
> Require Import gstep.
> Require Import gentree.
> Require Import gen_ext.
> Require Import rtcT.
> Require Import k4.
> Require Import k4_exch.
> Require Import k4_inv.
> Require Import k4_ctr.
>
> Cheers,
>
> Jeremy
>
> On 28/4/20 11:26 pm, Christian Doczkal wrote:
> > Hi
> >
> > > Anyhow, I've tried your suggestion:  I assume "-R/-Q" means choose
> > > either "-R" or "-Q" (without assuming this, coq_makefile produces 
> > > errors).
> >
> > Yes.
> >
> > > Then coq_makefile seems to work OK but then "make" produces the 
> > > following
> > >
> > > lots of warnings of which I show the last
> > > *** Warning: in file modal/k4.v, library lntacsT is required and has not
> > > been found in the loadpath!
> > > COQC lnt/tense-logic-in-Coq/cut_extraction_test.v
> >
> > Ah sorry, the syntax of -R and -Q is [-R physicalpath logicalpath] so
> > all three -R/-Q lines need a logical path as well (i.e., the prefix you
> > use in "From <prefix> Require Import <lib>). Something like TL, gen,...)
> >
> > The difference between -R and -Q is IIRC whether the files inside the
> > folder use the prefix when including other files from the same folder or
> > not.
> >
> > > Error: Invalid character '-' at beginning of identifier "-Q".
> > > make[1]: *** [Makefile:657:
> > > lnt/tense-logic-in-Coq/cut_extraction_test.vo] Error 1
> > > make: *** [Makefile:318: all] Error 2
> >
> > make is trying to use -Q as logical path, which obviously fails ...
> >
> > Hope this helps!
> > Christian