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

[Thomas Gazagnaire]

>>> The fact that you don't have a choice when installing a package to
>>> update all the package that may use it or not, is imho really
>>> frustrating. I have indeed had to recompile coq a few times as well,
>>> and the experience gets more annoying every time.
>> 
>> The solution for coq is to declare `labgtk` as an optional build-time dependency (eg. simply remove it from the list of optional link-time dependency, but let the right option in the configure invocation).
>> 
> 
> Interesting, it is quite simple.
> 
> But is it right that if you do that, when there is an important fix of lablgtk you will have to explicitly run "opam reinstall coq" and all the coq stdlib will be recompiled?
> 
> If it's true it is a nice and simple halfway solution.

If lablgtk does not appear in the list of dependencies (and optional dependencies), coq will never be recompiled automatically when you upgrade lablgtk. And if you do "opam reinstall coq" OPAM will indeed recompile the whole package.

Tracking dependencies at a finer grain that the package level requires build system hooks that OPAM doesn't have (yet?).

Best,
Thomas