[ocaml-platform] [Coq-Club] Coq opam package

[AUGER Cédric]

Le Wed, 10 Apr 2013 16:21:06 +0200,
François Bobot <francois.bobot at cea.fr> a écrit :

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

For coqide, it has a special make rule (make coqide) that you can run
after having build all the rest. Plus, although I am a Coqide user, many
do not use it and prefer Proof General, so I think that having a CoqIDE
target (which would depend on Coq) is relevant and trivial to do.

For the standard library, it is another matter, as AFAIK, *.vo files
use a magic number which must match the Coq version. So new Coq => new
compilation of the standard library.

A remark I did some years ago (and an opinion I still have) is that we
could have some "pre-compiler" which reads a *.v file and generate an
other *.v file (in pure Gallina syntax) in which there are only
Notations and Definitions (I mean there are no proof scripts anymore).

Those files should not change from a version to an other, excepted if
there is a modification on the standard library (and in this case, we
could pre-compile only the modified files). Compiling those files for
the new coq version should be (a lot?) faster as the terms would be
directly given. And to increase it even more there could be some binary
format instead of pure Gallina, but which format reflects Gallina
syntax and does not change from one Coq version to an other (and in
particular should not carry some magic number).

By the way, is there some significant change in vo files from a version
of Coq to an other ?