*** System ***
* Advanced support for Isabelle sessions and build management, see
"system" manual for the chapter of that name, especially the "isabelle
build" tool and its examples. Eventual INCOMPATIBILITY, as isabelle
usedir / make / makeall are rendered obsolete.
* Discontinued obsolete Isabelle/build script, it is superseded by the
regular isabelle build tool. For example:
isabelle build -s -b HOLCF
This refers to Isabelle/fb446a780d50 (and various changets before).
Further notes:
The last update of the Isabelle build process was done in December 1996,
when it was merely a matter of sitting there one afternoon to rework the
received Makefiles, which then became the classic IsaMakefiles. (The rest
of the Lehrstuhl was busy drinking Glühwein.)
This is now a major change, and hopefully a big step forward. Right now
there is a shadow version of new-style ROOT files of the current
IsaMakefile + ROOT.ML collection -- for the whole Isabelle distribution,
both src and doc-src. Note that the ROOT files are much easier to
maintain, but we need to keep both sides in sync a little longer until the
old usedir/makeall setup has been dismantled. (Hopefully very soon.)
In particular, we need to devise a plan to upgrade:
* isatest (Makarius?)
* mira (?)
* AFP (Gerwin and Makarius?)
I've tried to cover the needs for the testing infrastructures in the new
isabelle build tool to the best of my knowledge, but some details might
have been overlooked. (Florian might notice the option -s for "system
mode" to store heaps inside ISABELLE_HOME not ISABELLE_HOME_USER.)
For AFP, I would like to see a scheme without hardwired "document" option
within the ROOTs. Instead it can be provided for particular invocations of
"isabelle build -o document=pdf" etc. This and build -j MAX should give a
great speedup of everyday testing of AFP, with latex out of the way and
many cores busy.
The latter was in fact one of the motivations to get isabelle build done
right now, after so many years of delay, because AFP is becoming difficult
to manage with the classic collection of shell scripts.
Please see the fine system manual chapter that I have produced on the
spot.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
