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: Karl Crary <crary AT andrew.cmu.edu>
To: coq-club AT inria.fr, Théo Zimmermann <theo.zimmi AT gmail.com>
Subject: Re: [Coq-Club] How to make local sources take precedence over the library?
Date: Tue, 3 Sep 2019 14:44:42 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=crary AT andrew.cmu.edu; spf=Pass smtp.mailfrom=crary AT andrew.cmu.edu; spf=None smtp.helo=postmaster AT mail-qt1-f193.google.com
Ironport-phdr: 9a23:HKcfzxy5ZU1QFAXXCy+O+j09IxM/srCxBDY+r6Qd2+ofIJqq85mqBkHD//Il1AaPAdyBrasb0KGH7OjJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVmjaxe65+IRe4oAnessQbg5ZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8JtkqxbrhKvqR9xzYHab46aNuZxcKzGcNMGRmdMRNpdWzBPD46+aYYEEuoPPfxfr4n4v1YAqAGxBROoBOjy1DJInGX53bc60u88FgzJwBYgEMgUsHXUt9j6LqESXv2vzKbWwzTPde9Z2TLg6ITSbB8uvOyMUKt2fMHMx0cvEAbFgU+RqYzjJz6V1+INs3Ka7+V6T+6vhXQnpgdsqTas3schkpfFip4Rx1ze9ih0wJw5KcC5RUJne9KoDZ9dui+CO4drXs8uX3tktScgxrAJupO3ZjYGxZspyhPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq9Eiv0Oz8Vs2t3FZTsipJj8DAtn4Q2xHX5MWLUPR9/kCm2TaA0wDc9PtILlwzlareM5Ihw7gwmYQPsUnbACP6hEH7gLWVe0gk4OSk9uXqbqn8qpOBM4J5hBnyMqE0lcy+BeQ4PBIOX2+e+emkyLLj51f2QK9Kj/AtiKbZto3VJd4Fqa+3GQNazoMj6wulAzi4zdsYgGELLEhZdxKfk4jpJ1bOLejkAve4mlSgiStkx/TbPrL6GZjNNXjCkLL5fbln8UJcyQwzzcpe551OEL0BLujzCQfNs4nTCQZ8OAipyc7mDs9838UQQybHPq8YN5TgsFqN6/gqKu+KLNsJuDv6beok4vvvpXA8kF4ZO6Ku2M1ERmq/G6FFKl+dKVH2i80QWTMBpAMkXcTjjlGYXCEVbHOvGa8w+2doW8qdEY7fS9X10/S61yChE8gOPz0UOhW3CX7tMr68dbIMZSaVeJEzlzUFUf24V9Zk20j/70n1zL1oKueS8Sod58q6iIpFotbLnBR3zgRaStyH2jjTHWhyknkFWHk92b05rEBgmA/agPpIxsdAHNkW3MtnFwIzNJrS1et/Uo6gUwTNZNqWDl2jX5OrDSxjF98=

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?, Pierre Courtieu, 09/04/2019