The Coq mailing list

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

On 18/06/2013 13:48, Gabriel Scherer wrote:
> I ran into OPAM Coq recompilation one time too many, and created a
> (possibly alarmist) corresponding issue on the OPAM bugtracker:
>    https://github.com/OCamlPro/opam-repository/issues/805
>
>
> PS: François, I hope you won't be offended by the frustrated tone of
> the report. I very much appreciate the packaging work that you have
> done (and contributions to the tool itself !). I just don't think that
> OPAM is able to provide a good experience for the Coq package right
> now, so it probably shouldn't be, in its present form, in the default
> repository. I may also not be seeing the whole picture: if you or
> others have clear use-cases for using the OPAM packages of, say,
> Frama-C (as opposed to dumb binary releases for users and manual
> compilation for developpers), it would be interesting to explain them
> in the bugreport discussion.

Don't worry no offense taken. I didn't request a merge for the following 
commit (that extract coqide and its dependencies to another package and 
that would have saved your day) because it is more a hack than a real 
solution. I was looking for a better solution because I'm also 
frustrated ( today I have the pleasure to do opam upgrade
  - recompile camlp5.6.07 [upstream changes]
  - recompile coq.8.4pl1 [use camlp5]
)

Leaf project (in the dependency graph) like Frama-C are less a problem 
and since other project can depend on their libraries and binary 
(ex:Why2) its good to have them in opam. Moreover Frama-C takes only 
2min to compile.

> On Wed, Apr 17, 2013 at 11:43 AM, François 
> Bobot<francois.bobot AT cea.fr>
>   wrote:
> > https://github.com/bobot/opam-repository/commit/4c613c9c3bdd967785b7b251bf71c186203d28ca
> >
> > I tried to reduce the compilation time of the coqide package by patching the
> > Makefile. The coq package compile in 15min on my computer. 'make coqide'
> > compile in 2 min, I reduced it to 30s by removing many of the
> > ocamldep/coqdep/.ml4 uselessly done.
> >
> > branch coqide of 
> > git AT github.com:bobot/opam-repository.git
> >
> > If someone wants to make a try.
> >
> > --
> > François
> >
> > _______________________________________________
> > Platform mailing list
> > Platform AT lists.ocaml.org
> > http://lists.ocaml.org/listinfo/platform