The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 12/12/2013 05:47, Gregory Malecha wrote:

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

The standard library is a bit peculiar in that it is a set of libraries. 
So the "Coq" prefix should not be required. But accessing the inner 
files of the various libraries should require absolute paths (except for 
"Coq" again).

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

I think so. This would alleviate the idiotic naming of some of the 
libraries I contribute to: all the files of Gappa are prefixed by 
Gappa_; all the files of Flocq are prefixed by Fcore_, Fcalc_, Fappli_, 
Fprop_ depending on the subdirectory.

Still, I would add a small exception to the non-recursiveness. If a path 
happens to point to a directory rather than a file, a file with that 
name inside the directory should be selected. For instance, to load the 
Coquelicot library, the user should only have to do "Require Coquelicot" 
rather than "Require Coquelicot.Coquelicot".

Best regards,

Guillaume