Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing]
On Fri, 11 Oct 2013, René Neumann wrote:
While Gentoo supports slotting (i.e. multiple versions installed at
once), only a few packages are slotted, and also the slots might be too
wide for certain uses (e.g. jdks are slotted by 5,6,7,... and not by
minor version). Furthermore, depending on the package, consumers might
not work with multiple versions of a dependency installed (cf slotting
The same holds for configurations: A too restricted dependency (most
notable: needing to have a feature disabled) will quickly result in
So while Gentoo supports all those thing in theory, it would probably
not work out in practice.
These observations are consistent with my earlier guesses about the
culture and mindset of Gentoo packaging, or similar packaging communities.
Paradoxically, the "open-source bazaar" becomes centralized by the one big
arrangement of packages of a particular community (although there might be
ways to have alternative repositories, but this is again more complication
I see a fundamental conceptual problem here of operating system
distributions versus (against) application programs.
Moreover, I must confess that I am not very attached to a particular Linux
distribution nor its current brand, and tend to change the system
partiation quite often, while certain add-on applications remain happily
on /home. (This is out of necessity since no Linux version is really
stable these days.)
Interestingly, the Coq guys are presently discussing similar packaging
questions on the Coq-club thread "Package managing", e.g. see
https://sympa.inria.fr/sympa/arc/coq-club/2013-10/msg00096.html -- the
idea seems to be to delegate to OCaml package management (and thus become
subject to a particular INRIA-centric programming language world).
For Isabelle2013 and Isabelle2013-1-RC1 this privatized package management
is done in the weakest-possible sense: Isabelle "components" are bundled
with the one big application that you get from the Isabelle website.
There are no variants nor dependencies just one piece to be shipped, which
happens to be composed from a selection of parts according to the
specification in etc/components.
This tends to require a bit more disk space than necessary, but even just
one HOL image is already quite substantial compared to basic things like
Poly/ML or ATPs for Sledgehammer. Of course, JDK dwarfs everything else
and is as usual a problem on its own.
Using Isabelle professionally over some time, several GBs of disk space
can be easily filled with further heap images for the Isabelle
distribution, AFP, or other projects. This outperforms even JDK, despite
recent attempts of Oracle to inflate it again.
This archive was generated by a fusion of
Pipermail (Mailman edition) and