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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to