The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Thank you for the suggestion. 

> > 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 imagined that I could use a -pack option to organize name space, 
and possibly for (lightweight) visibility control 
by deliberately choosing which files to pack.
For instance, I may pack A.vo and B.vo into AB.vo, and A.vo and C.vo into 
AC.vo 
where A.vo, B.vo and C.vo are in the same directory;
well-designed packing could help to understand the program structure. 
But I might be naively thinking....
 
> > 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.

This will improve my life; thank you!

Best regards,
Keiko