[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
makarius at sketis.net
Wed May 30 22:01:04 CEST 2012
On Wed, 30 May 2012, Florian Haftmann wrote:
> This nukes the ancient idea of ~isabelle/contrib that you would just
> link it into your repository at TUM, regardless on which machine you are
> operating, and would get the best which has been achieved for that
> particular platform (whether the mechanism behind this are symlinks or
> Admin/contributed_components does not matter). I. e. if you have both
> you have to include either one by default, effectively restricting
> yourself to x86 or x86_32. Would it be impossible to provide those
> twins under one roof? Or is this distinction since they are not shipped
> both in one download bundle (as guess, I have not checked this)?
I realized after the Isabelle2012 release that the old contrib idea was
dead. When assembling the special platform bundles, I did remember that
it was done differently before, but was unsure how much of it was still
relevant. As the bundled distribution gets more and more sophisticated for
the end-user, the situation for non-releases gets more difficult. The gap
is widening with every release.
Not every component is equal in that sense, though. Especially JDK,
Poly/ML, jedit_build are all somehow special.
I don't see any problems providing "sliding versions" of jedit_build
components, and ~isabelle/contrib might have an almost complete history of
For Poly/ML the traditional scheme is to copy manually from the last
stable Isabelle release. It often needs to be changed in testing anyway.
For JDK I am still experimenting. Right after the release I have started
to make a more universal Linux JDK 1.7 for both x86 and x86_64, at the
cost of 150 MB extra disk space. (Surprisingly many Linux users get the
wrong download by default, even with our smart download button now.)
JDK 1.7 for Mac OS X is still an open problem. There are reasons to
believe that I can unify it with Linux before the next release.
JDK 1.7 for Windows is no problem, it is its own world anyway -- which is
actually a problem for the testing, but that is a completely different
More information about the isabelle-dev