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

[François Bobot]

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