Skip to Content.
Sympa Menu

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

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?


Chronological Thread 
  • 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
>>



Archive powered by MHonArc 2.6.18.

Top of Page