The Coq mailing list

[Johannes Waldmann <johannes AT albapasser.de>]

Dear all,

I am looking for some information or a tutorial on how (qualified)
Coq library names are mapped to locations in a file system,
and how this should be used to structure larger Coq projects.
It would be especially helpful to have a comparison to other languages
with hierarchical modules, e.g. Java or Haskell(-Prime).

I was starting with the naive expectation that "Require Foo.Bar.Baz"
leads to reading the file Foo/Bar/Baz.v(o)
and that writing out fully qualified names in each "Require"
implies that the Coq compiler *never* needs to seach for anything
(because it just opens the file, whose name can be computed).

It seems this behaviour can somehow be achieved with "-R Foo Foo"
or  'Add Rec LoadPath "Foo" as Foo' , but not quite:
it is then still possible to just do "Require Baz".

Can this (unqualified import) be switched off?
I think it is not needed (if all imports are written qualified)
and it has an implementation cost: all subdirectories will be
scanned during "Add Rec LoadPath", and that may include directories
that are not intended to be used in the current project
but contain files that will confuse the compiler
(if they accidentally have overlapping names).

In fact that was the starting point of a little debate on
the Color mailing list, see this thread here
http://websympa.loria.fr/wwsympa/arc/color/2008-06/msg00013.html
and it was suggested to ask on coq-club for advice.

Thanks - Johannes Waldmann.