[isabelle-dev] NEWS: Isabelle sessions and build management

[Makarius]

*** 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