There is too much shadowing of standard modules

[jwiegley]

Because ext-lib defines modules like Bool, I've found that when you have ext-lib installed globally, it shadows too many of the standard modules for developments which just Require Bool. For example, Software Foundations cannot compile in the presence of coq-ext-lib. I've run into such discrepancies in other projects as well, where because of the presence of ext-lib (even though I never asked to use ext-lib), it was causing compilation behavior to differ between multiple environments. Finally I had to uninstall ext-lib just to keep a sane environment.

So my recommendation is to employ some mechanism to avoid shadowing anything that might be implicitly imported from the stdlib, like bools and tuples.

[gmalecha]

This is supposed to be fixed in 8.5 when libraries will not be included with -R (which itself is horribly broken). Until that fix is in I have been requiring ExtLib locally for projects using _CoqProject or .dir-locals.el and requiring it with -I, e.g. -I <path-to-ext-lib-theories> -as ExtLib. This makes it so that you can Require Import Bool and get Coq's Bool and you can Require Import ExtLib.Data.Bool to get ExtLib's definitions surrounding bool.

The only solution that seems to work in 8.4 would be to prefix every file with something, e.g. Bool -> ELBool or something like that which just seems very ugly to me. That is the purpose of namespacing modules.

Alternatively, you can tweak the Software foundations using some scripts to make them require full Coq paths, e.g. convert Require Import Bool to Require Import Coq.Bool.Bool.

What do you think is the best solution?

[jwiegley]

If 8.5 is going to resolve this question, then I think just waiting for 8.5 is the best solution. :)

[gmalecha]

From what I've heard it will not include user-contrib using -R which will solve the problem.

[gmalecha]

This is solved in 8.5