The Coq mailing list

[Sylvain Le Gall <sylvain+ocaml AT le-gall.net>]

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