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

Gabriel Scherer gabriel.scherer at gmail.com
Tue Jun 18 12:48:25 BST 2013


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


More information about the Platform mailing list