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: Pierre Courtieu <pierre.courtieu 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 11:24:57 +0200
Authentication-results: mail3-smtp-sop.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-f47.google.com
Ironport-phdr: 9a23:Q1FhSRFltqjD+0WqeD4sbp1GYnF86YWxBRYc798ds5kLTJ78rs+wAkXT6L1XgUPTWs2DsrQY0rCQ6v+9EjVbqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAnctMkbjYR/Jqs/1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIOMuZWrYbzp1UAoxijCweyGOzhxSRFhmPv3aAgz+gtDR3K0Q4mEtkTsHrUttL1NKIKXO6vzanH0y/Db+lI1jzg9oXIdQ0hoeuQXbJxb8XR1FQkGgTdjlWRt4PlJSmV2foXv2eH6OpgSPivi3Imqw5vvzii3cgsiozTiYIUzlDI7zl2wIEwJdChTkNwfN2qEINIui2EK4d7RtkuTmJotSog17ELuJ+2cDIFxZklwRPUduaJfJKS4h35UeacOTd4i2xheLK4nxuy9FKvyuz4VsWt0VZKqTdJnsDCtn0C1RHf8MeHSvx6/keu3TaAyRrf5f1DIUAxjabbKpghzaAslpcLr0jPAiv7lF/1gaKWbEko5+ml5uX9brjppJKQL4p0hRv/MqQqlMy/G+M4Mg0WUmiD+OSzyqfj/VfnT7lQkvI2lbTZsIrGJcQauKG5HhRY0okm6xmlDjem1M4UkmUALFJAYB6HlZTmO0nSIPDkCveym0ijkDByx/zfIrLhBojNIWPYnbf6fbd97lZcxxApwdBe4ZJUELABL+jpVk//rtyLRiM+Ziez2q7MDMh3ntcVXnvKCauEOovTt0WJ76QhOb/fSpUSvWPFKvU//fOmpngkg0MccLThiYMWZWqiE7JtJFiDfXvhn/8OFG4Lukw1S+m82w7KaiJae3vnB/F03To8Eo/zSN6bHtn80ozE5z+yG9htXk4DD1mNFXnycIDdAqUDbSuTJolqlTlWDOH8Gb9k7gmnsUrB85QiLufQ/XdF55fq1dww5uqK0B9uqnp7CMOS12zLRGZxzDtRG20GmZtnqEk48W+tlLBiiqUBR9NW7vJNFAw9MMyEwg==

Le mer. 4 sept. 2019 à 11:01, Karl Crary
<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

Yes you need to compile Foo.v with an option (-R <dirname> Here
probably). Hence the need for a _CoqProject file.
Like Théo said: forget about Add LoadPath, just write the good -R
option in _CoqProject file and you won't need it.

P.

[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