The Coq mailing list

[François Bobot <francois.bobot AT cea.fr>]

Hi,

	Opam is a source-base package manager (1). It simplifies a lot the 
compilation and installation of ocaml tools and libraries but more 
importantly it helps managing the dependencies.

	I'm maintaining some packages (ie. Why3 and Frama-c packages (2)). 
Since some depend on Coq I also try to keep the Coq package up-to-date 
(3) (If someone of the Coq team wants to maintain it, it is quite easy, 
I can provide links, explanations and helps).

	I have naive questions about possibilities to mitigate the time spend 
by the compilation of Coq. Opam is source-based so you have to compile 
the Coq standard library. Moreover when a dependency of Coq change Opam 
trigger a recompilation of the package. When it is Lablgtk that changed 
the compilation of the standard library is needlessly made again. 
Lablgtk can change often because many C library are optional.

 - Is it possible to compile coqide once (make bin/coqide) and the rest 
of Coq during another compilation (2 packages)?
 - Is it possible to precompiled the standard library for specific 
ocaml versions? Then only check it with coqchk?
 - Another way?

Thank you,

Best,

(1) http://opam.ocamlpro.com/index.html
(2) http://opam.ocamlpro.com/pkg/why3.0.81.html
(3) http://opam.ocamlpro.com/pkg/coq.8.4pl1.html


--
François Bobot