The Coq mailing list

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

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