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

[Anil Madhavapeddy]

Since OPAM is currently a conservative source-based package manager,
it's hard to escape recompiles of packages if something genuinely changes
upstream in the dependency chain.

The only solutions are to go OPAM more insight into the dependency graph
of package contents (which is ongoing, but will take some time), and
to break up packages into smaller chunks.

Therefore, I've updated your bug report with a request for François's
split package for Coq and Coq-IDE, which will remove the IDE dependency
entirely from the core Coq package.  OPAM's dependencies will ensure that
Coq-IDE stays precisely in sync with the version of Coq that's installed.

-anil

On 18 Jun 2013, at 12:48, Gabriel Scherer <gabriel.scherer at gmail.com> 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.
> 
> 
> On Wed, Apr 17, 2013 at 11:43 AM, François Bobot <francois.bobot at cea.fr> wrote:
>> On 11/04/2013 00:12, Wojciech Meyer wrote:
>>> Anil Madhavapeddy<anil at recoil.org>  writes:
>> 
>>> I think the biggest chalenge here would be to make people to use this
>>> techniques (splitting bigger packages) when it's not always clear how
>>> it
>>> should be done. I already started to think that Coq IDE deserves a
>>> separate OPAM package, and my worry is that it's bit unclear how to do
>>> this. So maybe theorems, could be also decoupled and put under
>>> different
>>> name. Otherwise I agree, it would better.
>> 
>> I extracted coqide into its own package.
>> 
>> 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
> _______________________________________________
> Platform mailing list
> Platform at lists.ocaml.org
> http://lists.ocaml.org/listinfo/platform
>