The Coq mailing list

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

Hi Pierre,

Well, I want to do something that is easy and works, like (in Coq 8.11)
Add LoadPath "../tense-lns".

I got the impression that this is somewhat like using an empty logical 
name for the directory, but I don't want to get hung up on terminology.

I don't suppose this possibility was removed solely because it made 
things possible/easy for the users, so I would be curious to know the 
reasons.

I think perhaps the concept you mention ("logical names") is related to 
the errors I got before such as

The file /home/jeremy/coq/lnt/tense-logic-in-Coq/genT.vo contains 
library genT and not library xx.genT

when I was trying to use CoqProject with all the suggestions various 
people made.  Would that be correct?  Is "xx" here, or the absence of 
it, a "logical name"?  And how does one compile a Coq file (genT.v) to 
make it contain the library xx.genT rather than the library genT?
And (I know I must sound like a broken record here, but I'm just as sick 
of it as anyone reading it) is this anywhere in the documentation?

About an archive of the whole setup, my email a few minutes ago 
addresses this.

Thanks for any help,

Jeremy



On 20/1/21 5:21 am, Pierre Courtieu wrote:
> Jeremy Hi,
> Yes, it would be nice to see somewhere an archive of your whole setup,
> so that we determine exactly what makes it incompatible with
> _coqProject and coq_makefile.
> I think the reason is that you don't want to use logical names for the
> different directories you have, but IIUC this is more or less
> mandatory.
>
> Best regards,
> Pierre
>
>
> Le mar. 19 janv. 2021 à 16:24, Yannick Forster <yannick AT yforster.de> a écrit :
> > Hi Jeremy,
> >
> > what's the error message you get? Is your code publically available (on 
> > github or something similar)?
> >
> > Best
> > Yannick
> >
> > On 19 January 2021 13:52:24 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:
> >
> > > Hi,
> > >
> > > I have just upgraded my operating system, which has also involved
> > > getting Coq 8.12.2 (December 2020)
> > >
> > > Previously I was using Coq 8.11.2
> > >
> > > The command
> > > Add LoadPath "../tense-lns".
> > > now seems to cause an error.
> > >
> > > How do I change the command to get the same behaviour?
> > >
> > > Thanks
> > >
> > > Jeremy