The Coq mailing list

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

Hi Gaetan,

Thanks for your advice: I don't quite know how best to make this clear 
but I want something that works.

At present, even if I have to recompile 20 or 30 files whenever I change 
one of them, that is preferable to trying a myriad of different things, 
as I have been doing in the last day or so.

So here is the situation.  I have a bunch of coq source files, not all 
in the same directory, in most cases depending on other source files.

If anyone knows whether the _CoqProject and coq_makefile capabilities 
handle this situation, and knows how to do it, and is able to tell me 
how, I'd appreciate it.  (with the further limitation that I'm not 
touching the existing Makefile or any of the source files in 
../lnt/tense-logic-in-Coq because it works and is not used solely by me).

Otherwise please don't advise people like me to use it, it just wastes 
everyone's time.

Thanks

Jeremy

On 28/4/20 11:45 pm, Gaëtan Gilbert wrote:
> 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