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

[Sylvain Le Gall]

2013/4/11 Thomas Gazagnaire <thomas at ocamlpro.com>:
>>>> 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?).
>

Isn't it possible to keep the compiled source tree (i.e. just what you
got before make install) and restart with a "make all". If it fails
and you know you try to resume from the middle, just start again with
"make clean; configure && make all".

If the build system supports detecting changes in external libraries,
this should be fine and you'll be able to incrementally recompile coq
-- if not, you fallback to the default mode. In other words, you move
the problem to the build system without any hooks. I am pretty sure
this is not supported by ocamlbuild, but it can be good incentive to
create something that works this way.

Cheers
Sylvain