The Coq mailing list

[frederic.blanqui AT loria.fr]

On Wed, 18 Jun 2008, Keiko Nakata wrote:

> Is there a tool or extension which packs several Coq object files into a 
> single file
> containing the object files as sub-modules, a la Ocaml's -pack option?

i am not sure whether you need such an option in coq: in contrast with ocamlc, 
there is no linking phase in coqc.

> > 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.
>
> I have been having the same and related problems.
> I had several files with the same name and used the file system's hierarchy
> to organize the name space. Then my life became complicated;
> I miss at least the -pack option as supported in Ocaml.
> (the -pack option combines specified object files, packing them in a single 
> file
> containing the object files as sub-modules:
> http://caml.inria.fr/pub/docs/manual-ocaml/manual022.html)
>
> I ended up in giving distinct names to distinct files;
> my life has become easier, but I am not very happy.

this is also the solution we adopted in http://color.loria.fr/. and to make 
the life even easier, every thing is compiled using the option

-R <directory_where_CoLoR_is> CoLoR

(instead of using many options like "-I dir" or "-I dir/subdir" etc.)

after that, people willing to import CoLoR modules just have to use this 
option too, or to use the following command:

Add Rec LoadPath "<directory_where_CoLoR_is" as CoLoR.

which can be put in the ~/.coqrc file.