The Coq mailing list

[Wojciech Meyer <wojciech.meyer AT gmail.com>]

Anil Madhavapeddy 
<anil AT recoil.org>
 writes:

> The issue with not recompiling dependent packages immediately is
> that you leave your build environment with inconsistent packages
> (since the library CRCs may no longer match).  OPAM is conservative
> about not breaking ABI invariants by default, which seems wiser than
> a few unnecessary recompilations at this stage.
>
> I'd be inclined to figure out a mechanism to decouple Coq IDE from
> Coq in the packaging a little more, rather than complicate the
> optional dependency constraint analysis even more.

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.

-Wojciech