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 boost).

The same holds for configurations: A too restricted dependency (most notable: needing to have a feature disabled) will quickly result in trouble.

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 than necessary).

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 -- 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 MHonArc.