[isabelle-dev] Poly/ML

[Makarius]

On Tue, 21 Jun 2011, Clemens Ballarin wrote:

> The Isabelle download page is surprisingly silent about Poly/ML 
> nowadays.

The deeper reason for that is the tendency towards "no servicable parts 
inside", i.e. the default bundle contains already (almost) everything one 
needs, included all the add-ons.  Assembling things by hand has become 
quite difficult, it usually takes 1-2 weeks before each release to do it.

The bundle introduces some bloat concerning harddisk space and download 
bandwidth.  I think there is no practical problem with diskspace, and the 
download might get more slim in the near future thanks to "xz" 
compression, which I have recently discovered as replacement for the older 
"gz" and "bz2".  There is a pure JVM module for xz decompression (much 
faster than the gz one from Sun/Oracle), so that might become part of our 
Scala infrastructure somehow.


 	Makarius