coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Add LoadPath in Coq 8.12.2

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Add LoadPath in Coq 8.12.2
Date: Tue, 19 Jan 2021 19:21:50 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f53.google.com
Ironport-phdr: 9a23:CdqU4R8EGNaF/P9uRHKM819IXTAuvvDOBiVQ1KB20u4cTK2v8tzYMVDF4r011RmVBNSdsqoP1Lae8/i5HzBZvtDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAHcutMLjYd+Jao8yBTEqWZMd+hK2G9kP12ekwv+68uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjZa7WY88USnRdUcZQTyxBA52zb40TD+oaIO1Uq5Dxq0YSoReiAAWhAv7kxD1ViX/sxaA13OohHgPG0gIuHNwArWrao8n6OqoJTeC11bPFwSnfY/9K2zrw7pXDfBA7ofGLWLJ9adDfyUgxGAPflFWft5HuMi2S1uQQqWib8+tgWvyyi2U6rAxxujmvydk2ionTmI0Z0EzL9SJkwIYvOd24SVB0YcO/HZtfsiGVLYp2Qsc4T250vyY6z6QLtJimdycF1Jop3QTQa+Cbc4eW+BLjUv6cLClmiHxleL+ymgq+/FSvxOD8S8S5zFdHozRLn9TDuX4A1QDf58mDR/Vz4EutxDSC2Q7O5+9LIU44iLfWJp0uz7M2i5EdslzDEzfolEnqiKKabEYp9+iy5+j6Y7jrp4WQOo96hwz4L68ggNawAf4iPQgLR2Wb+fqz1Lnk/UDhRbVFlPw2kq3AvJDbIsQXu7e1AwFV34st8Rq/ADCm0NMXnXkDMl1JYg6Ij4/sO13WIfD4C+mwg0i0nTt12/zLOqftD5bNI3TZjbvsfLdw51RcxQc91dxf4ohbCrAFIPL9QE/xs9nYAwchMwy13ennEs992Z0EVW2TBa+ZLbnSsUOJ5u0xPumBf4AVuDPnJPgk4/7il2M2mVgYfaWxx5sYdGi4Huh6I0WeeXfjntABEX4TsgUiSOzqlUaNXCVIZ3eyWqI8/is0BJinDYfFXICtgaaO0D21Hp1MNSh6DQWnFm6gXIGZUb9YYyWLZ8RljzYsVL67SoZn2wv45yHgzL8yFuvZ4DcV/bnkycJp5uDO3UUq9DFuFcnb2GaQVX11k34gSDo/3aQ5qkt4nATQmZNkiuBVQIQAr8hCVR03YNuFl7QjVoLCHznZd9LMc26IB9WrBTZrE4A0yt4KJkd6QpCs00uF0C2tDLsY0beMAc5sq/OO7z3KP894jk3++uwkhlgiTNFIMDT/1KF6/gnXQYXOlhfAzvr4ReEnxCfIsVy74y+WpkgBCVx/VKzEWTYUYU6E9dk=

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
>
>

[Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/19/2021
- Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Clément Pit-Claudel, 01/19/2021
  - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/19/2021
    - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Clément Pit-Claudel, 01/19/2021
- Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Yannick Forster, 01/19/2021
  - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Pierre Courtieu, 01/19/2021
    - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/20/2021
      - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Guillaume Melquiond, 01/20/2021
        
        Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/20/2021
        
        Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Yannick Forster, 01/20/2021
        
        Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Pierre Courtieu, 01/20/2021
  - Re: [Coq-Club] Add LoadPath in Coq 8.12.2, Jeremy Dawson, 01/20/2021