coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: Karl Crary <crary AT andrew.cmu.edu>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to make local sources take precedence over the library?
- Date: Tue, 3 Sep 2019 22:59:00 +0200
- Authentication-results: mail2-smtp-roc.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-vs1-f66.google.com
- Ironport-phdr: 9a23:AVP16xfW2J/sDBE8ElyYHgX2lGMj4u6mDksu8pMizoh2WeGdxcS6bB7h7PlgxGXEQZ/co6odzbaP6ea5BjdLuMzd+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLq8Ubg4VvJqksxhfXrXZDZvhby35vKV+PhRj3+92+/IRk8yReuvIh89BPXKDndKkmTrJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4qJ2QxLmlCsLKzg0+3zMh8dukKxUvg6upx1nw47Vfo6VMuZ+frjAdt8eXGZNQ9pdWzBEDo66coABDfcOPfxAoobyqVsBrxuwCwevCu3y1DFHmmT70rcm3+k7CwzKwBAsEtAIvX/JrNv1LqASUeWtwafWzTXEdfRW1i/+54jJdxAhpO+DXah1ccXLz0kvER7Og1KMqYzlITyV0f4Bsmma7+plUOKvinUqqw50oje1x8csjpPFiZ4SylDB7Ch0xps+K9O/SE5+e9GkEZ1QujmbN4twWMMiQntntDw0yr0cv5OwYSsEyIw/yhLBd/CKd5KE7xHjWeqLPzt0mXBodKi+ihuz90Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWHT+Fy/kal2TqWyQDT8fxILVk6lafaKpMt2LEwlp0UsUTMGi/5hl/6g7ORdkUh4uSo6uLnbav6ppKEKYN4lgXzPr4tl8G/G+g0LBUCUmqB9em91bDv5Uj5T69Ljv0ynKnZqpfaJcEDq66lAw9azIEj5wy+Djen1dQYmHgHIUlKeBKClYfpOlXOLOrkAve4hlSgiC1ryOzePr39HpXNKWDOn6vmfbZk8kJT1A4zzc1E6J9PEbEAIPfzWlfru9DCDx85NRa0w+f9B9ln2IMeQzHHPqjME6rItRej/Os1MqHYb5UcoifVIv4p/fPxy3Q8hBkQcbT/jrUNb3XtIvTnJHKrYH/pj80EGGEM9l4iTOHtzk+DVDtST3m3VqM4oDo8DdT1Xs/4WomxjenZj2+AFZpMazUDUwjUSCq6R8C/Q/4JLRmqDIphnzgDD+XzToYg0VSwr1a/xeQ5aOXT/SIcuNTo090nv7SCxyF3ziR9CoGm60/ISmh1mm0SQDpvhfJwpEV8zhGI1q0q2qUER+wW3OtAV0IBDbCZ1/ZzUomgVQfIf9PPQ1GjEI2r
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> 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> 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?, Maxime Dénès, 09/04/2019
- Re: [Coq-Club] How to make local sources take precedence over the library?, Pierre Courtieu, 09/04/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
Archive powered by MHonArc 2.6.18.