coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make local sources take precedence over the library?

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to make local sources take precedence over the library?
Date: Wed, 4 Sep 2019 12:19:46 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f65.google.com
Ironport-phdr: 9a23:Grw62BEsMNgcZeXb5hT5k51GYnF86YWxBRYc798ds5kLTJ7zp8ywAkXT6L1XgUPTWs2DsrQY0rCQ6v+9EjZcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAnctMkbjYR8Jqs+1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIOMuZWrYbzp1UAoxijCweyGOzi0SVHimPs0KAgz+gtDQPL0Qo9FNwOqnTUq9D1Ob8MX+C11q7Iyi3MYPBX2Tf47YjHbAohofSWUrJ2d8ra1E4iFx/FjlqOrozpJTKU1uUIs2ie7uptTu2vi2s9pAFwpjij3Nsjio7Mho8MzF3P6Ct3wIEwJdKiSU57Z8apEJpWtyGANot5WNkuQ29yuCs817YIuoa7cTAUxJg7wxPTcf+KfoiS7h79SuqdPy10iXNldb+5mh2861KvyvfmWcmxyFtKrjRKkt3Ltn0V0hzc8MmHSv9k8ke8wzmDyhnf6u9FLE00j6bbJJkhwrk/lpoXr0vPBDP5mELzjKOOd0Uk/Pan6/j/b7n4upORM5V4hwL+P6g0hMCzH/o0PhIPUmWb4ei80afs/Uz9QLVElP02lazZvYjGJcQbuKG5BBVZ04ci6xa6Cjem0c8VnXYCLF1feRKHi5LlNE3JIPD9Ffu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDEmIG+eyNL7Y+QuD4ftqKO2RbqcUviz8Ir4r/ai9o2U+nAohfSiu6qkWbXW1BPFvJUPRNWbsj9BHA2YPuwsWQ+njiVnEWjlWMSXhF5kg7y02Xdr1RbzIQZqg1fnYhH/iQ89mI1teA1XJKk/GMoWJX/BWNXCXK85l1yENDP2vFdJn2hapuwv3jbFgK7iMo3FKhdfYzNFwotbru1Qq7zUtVpaS1miMSyd/mWZaH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQC1U1MJfdy6pxDNWgAw8=

Hi Maxime,

I have wondered the same and thought that maybe it has some valid use cases in some corner cases. For instance, I think there is an rcfile feature where people can put some Coq commands. I suppose we would need to deprecate both features together.

Théo

Le mer. 4 sept. 2019 à 11:38, Maxime Dénès <mail AT maximedenes.fr> a écrit :

Hi Théo,

I fully agree with your advice, by why don't we deprecate `Add
LoadPath`, then?

Maxime.

On 9/3/19 10:59 PM, Théo Zimmermann wrote:
> Hi again,
>
> I strongly recommend you never use Add LoadPath. Instead, you should use
> a _CoqProject file containing a single -R or -Q directive. From there
> you can use coq_makefile to generate a Makefile to compile your project.
> The _CoqProject file is also understood by Proof General and CoqIDE, so
> from there it should all work out of the box.
>
> I would link you to the documentation, but I'm on my phone so it's a bit
> difficult.
>
> Théo
>
>
> Le mar. 3 sept. 2019 à 20:44, Karl Crary <crary AT andrew.cmu.edu
> <mailto:crary AT andrew.cmu.edu>> a écrit :
>
> Hmm. This doesn't quite seem to do what I want. I'm trying:
>
> Add LoadPath "." as Here.
> From Here Require Import Foo.
>
> and I get:
>
> The file .../Foo.vo contains library Foo and not library Here.Foo
>
> -- Karl Crary
>
>
> On 9/3/2019 12:34 PM, Théo Zimmermann wrote:
> > Hi,
> >
> > If the collision occurs at Require Import time, you can use the From
> > prefix to specify that the module should be found in your own project
> > instead of Coq's library.
> > Cf.
> https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmdv.require-import
> >
> > Théo
> >
> > Le mar. 3 sept. 2019 à 18:31, Karl Crary <crary AT andrew.cmu.edu
> <mailto:crary AT andrew.cmu.edu>> a écrit :
> >>
> >> Hi all,
> >>
> >> I upgraded to 8.9.1, and found that several new modules have been
> added
> >> to the library whose names collide with my own. Unfortunately, this
> >> breaks my code in many places. Is there a way to tell Coq to give
> >> precedence to local sources over libraries?
> >>
> >> Thanks for any help.
> >>
> >> -- Karl Crary
> >>
>

[Coq-Club] How to make local sources take precedence over the library?, Karl Crary, 09/03/2019
- Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/03/2019
  - Re: [Coq-Club] How to make local sources take precedence over the library?, Karl Crary, 09/03/2019
    - Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/03/2019
      - Re: [Coq-Club] How to make local sources take precedence over the library?, Maxime Dénès, 09/04/2019
        
        Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/04/2019
      - Re: [Coq-Club] How to make local sources take precedence over the library?, Robbert Krebbers, 09/04/2019
        
        Re: [Coq-Club] How to make local sources take precedence over the library?, Théo Zimmermann, 09/04/2019
    - Re: [Coq-Club] How to make local sources take precedence over the library?, Pierre Courtieu, 09/04/2019