The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

My opinion on this.


On Thu, Dec 12, 2013 at 5:47 AM, Gregory Malecha
<gmalecha AT cs.harvard.edu>
 wrote:
> Hello --
> [...]
> 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).

It's even worse in case-insensitive file systems(*).  For instance,
recompiling Coq with the Ssreflect library is impossible because
Vector gets confused with vector.

(*) In my opinion they shouldn't exist, but thanks to the two ex-young
entrepreneurs from Silicon Valley, they do!

> 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?

Definitively.

> If so, should we special-case the standard library in some way so it does
> not require absolute names?

I prefer not.  The less exceptions, the cleaner.

> 2) Should Coq file resolution be changed to not be recursive by default?
>

Absolutely.


> 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/