The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

(First, let me announce that nothing about OPAM for Coq has been
announced, so please, do not consider this an announcement. Better
things are coming, stay tuned.)

Then, the problem Gregory reports seems really serious to me too, and
crops in many places. If packages become used, then having non
absolute names will makes us hit a wall soon. (Or  everyone one will
use small strings as prefixes of module names, e.g. ssr.)

I would argue that it is mandatory to change the default behavior as
soon as possible: use absolute names, and make path resolution non
recursive.

Thomas



On Thu, Dec 12, 2013 at 5:47 AM, Gregory Malecha
<gmalecha AT cs.harvard.edu>
 wrote:
> Hello --
>
> I'd like to start by saying that I think that Thomas Braibant's port of opam
> (https://github.com/braibant/opam) to work with Coq is a great step towards
> actually building up a shared repository of Coq code that is easy to use.
>
> Now I'd like to bring up a point that has recently bitten me for which I
> don't know a good clean fix for but I think is an important thing to think
> about if this type of repository is to exist.
>
> Coq currently uses a "recursive import" model of includes where users use
> '-R <path> Foo' to refer to the files in <path>. While these can be required
> using
>
> Require Foo.Xxx.
>
> it is common practice to elide the Foo. and instead just write:
>
> Require Xxx.
>
> This works reasonably well in most cases but starts to fall apart when two
> files (in two completely different packages) have the same name. I found
> this with a library that I have been working on called coq-ext-lib
> (https://github.com/coq-ext-lib/coq-ext-lib) which, when compiled, contains
> a file: ExtLib.Data.Bool. As soon as you install this package all of your
> current files which
>
> Require Import Bool.
>
> which previously referred to Coq.Bool.Bool will now refer to this
> ExtLib.Data.Bool. This is obviously a bad thing (since the user doesn't see
> it, spooky action at a distance).
>
> I am wondering what the Coq community thinks about this issue. I can think
> of two solutions/work-arounds:
> 1) Should it become best-practice to include files by their absolute names?
> If so, should we special-case the standard library in some way so it does
> not require absolute names?
> 2) Should Coq file resolution be changed to not be recursive by default?
>
> Are there other solutions? I am happy to work on the code to make whatever
> people think is the best approach a reality. I have already developed a
> small Coq patch that extends vernacular command with [From ... Require ...]
> which would alleviate some of the headache of absolute paths. I've submitted
> a Coq feature request (with the patch) here
> (https://coq.inria.fr/bugs/show_bug.cgi?id=3184).
>
> I look forward to hearing people's feedback.
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/