[isabelle-dev] Isabelle build and jedit startup

Makarius makarius at sketis.net
Fri Dec 7 18:36:16 CET 2012


In Isabelle/7c8ce63a3c00 from today, the isabelle build dependency check 
should be a bit faster, although I had to disable the parallelization 
again, because it is unstable in scala-2.9.2 (in scala-2.10.0.RC3 it 
appears to work).

This is relevant for Isabelle/jEdit users, because the selected logic 
session is now checked and built on startup.  The idea is that we ship 
without pre-built images, and they are produced on the spot.  This avoids 
an early decision about the actual platform: most Linux users don't know 
if they have 32 or 64 bit, or when they have 64bit of the 32bit C/C++ 
libraries are installed.

It was technicality impossible in the past to build logic images on the 
spot, due to the dependence on "make", which does not exist by default, 
and if it is there it fails to work with spaces in ISABELLE_HOME.

Another consequence: it is now more easy to switch logic sessions, say 
HOLCF, HOL-Word, HOL-Nominal.


A slight disadvantage of the current setup is that choosing a "bad" 
session (just for curiosity) might give a penalty of several minutes build 
time on the next start, before the session can be switched back again. (An 
escape is to say "Cancel" and edit $ISABELLE_HOME_USER/etc/preferences by 
hand.)

The little build dialog could be smarter here, but I have already spent 
much more time than anticipated on this tiny little thing.


 	Makarius


More information about the isabelle-dev mailing list