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 13:44:35 +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-f54.google.com
Ironport-phdr: 9a23:pbT8OBR9zsyVJbH07Nx4a7/Xq9psv+yvbD5Q0YIujvd0So/mwa69YhyN2/xhgRfzUJnB7Loc0qyK6vqmADNdqsrZ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLq8Ubg4tvJqk+xxfVv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/XrJgcJskq1UvBOhpwR+w4HKZoGVKOF+db7Zcd8DWGZNQtpdWylHD4ihbYUAEvABMP5XoInzpVQArRWwCwqxCu3x1jBGiWT73bEj0+k7DQ3KwBAsEtAIvX/JrNv1LqASUeWtwafWzTXEdfRW1i/+54jJdxAhpO+DXah1ccXLz0kvER7Og1KMqYzlITyV0f4Bsmma7+plUOKvinUqqw50oje1x8csjpPFiZ4SylDB7Ch0xps+K96gSENjf9KoDJ9duzuZOoZ2WM8uXXxktSQgxrAGtpO2ejUBxo49yB7FcfOHdpCF4hL9W+aVJjd1nHdld6i+hxa26ESg1Pb8WtSt3FZEridIncPAtn8K1xzU5ciHTuVy8l291jaI0gDf8uBEIUYqmqrHM5Mt3KI8m54JvUnAHiL6glv6gLKUe0k++uWl5PzrYrD8qZ+dM490hBv+MqMrmsGnHeQ4MhYBX2+B9eW91b3j+Ej5QLRRg/05l6nWqpHaJcABqqGlBA9V154v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4Md/DahJC/buUAelv9vBSxQ9LgacwuD9Cdw72JlICkyVBarMDKNTtmi65+cqLvOJbYkT8GLhK/UioezviHo4sVAYdKitm5AQbSbrTbxdP0yFbC+00Z86GmAQs197FbSy0QzQYXtof3+3GpkEyHQ+AYOiA53EQ9n00rOE1Sa/WJZRYzIfUwzeITLTb4yBHsw0RmeKOMY4y24LULGgT8kq0hT87FanmYoiFfLd/2gjjbym1NVx4LeOxxQ79DgxEd/Elm/QEyd7mWQHQzJw16d68xRw

Compatibility mainly. I can easily recommend a user to switch to a
_CoqProject file using a -R directive. If I jump over -R directly to
-Q, they will just have a harder time and won't listen to my advice.

Le mer. 4 sept. 2019 à 13:18, Robbert Krebbers
<mailinglists AT robbertkrebbers.nl>
a écrit :
>
> On 9/3/19 10:59 PM, Théo Zimmermann wrote:
> > I strongly recommend you never use Add LoadPath. Instead, you should use
> > a _CoqProject file containing a single -R or -Q directive.
>
> What is the reason why one should use the -R directive, ever? Shouldn't
> it be deprecated in favor of -Q?

[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