Re: [isabelle] Isabelle on OpenBSD?



On Wed, 16 May 2012, Timothy Bourke wrote:

In my opinion, a reasonable compromise may be to port Poly/ML and to download the Isabelle source directly.

This used to be the classic way until 2007 or 2008. Then more and more add-on tools were made available by default. Isabelle2012 already approximates some kind of operating system distribution for logic-based tools, with SPASS, E, Z3 etc.

I've also taken away the freedom to choose a JVM -- a particular version is bundled by default. This investment of 150 MB extra disk space solves a lot of problems of everybody. E.g. I've first had both Java 6 and Java 7 as an option for Isabelle2012, but after some months a few dropouts in jEdit on Java 7 (update 4) were discovered, so it is back to the 1.6 now. For the next release after Isabelle2012, another JVM will be taken on board, independently of any other JVMs that might be installed elsewhere.

For Windows I also bundle a full Cygwin installation at merely 99 MB. That's a real bargain compared to the logic image sizes:

  HOL 32bit: 140 MB
  HOL 64bit: 280 MB

That is the default heap environment that the user needs to download (compressed) and unpack -- as part of the main bundle. It takes in the range of minutes to do so.

Since the coming Poly/ML release is anticipated to be very fast in building HOL and producing the image -- and when we've finally abolished the dependency of "make" in the build process -- the logic images could be built on the spot after download.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.