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

[Makarius]

This is an update on the build configuration for AFP:

   Isabelle/4dd1d4585902
   AFP/4892fed712e1
   afp-build/a6ccf93b0574 (see https://bitbucket.org/makarius/afp-build)

The Scala and ML functions of afp-build guess the content of the original 
ROOT.ML and IsaMakefiles, and turn them into afp-devel/thys/ROOT -- the 
result is already committed to AFP for experimentation (it should not be 
editing right now).

Note that the configuration of AFP as Isabelle component does *not* 
include this large session name space by default.  Instead there is a 
separate isabelle build_afp tool, which provides access to it with some 
default options for regular isabelle build to produce browser_info and 
pdf documents.

Example:

   * edit $ISABELLE_HOME_USER/etc/settings:

       init_component "/some/where/afp-devel"

   * shell:

       isabelle build_afp -A -- -j4 -o threads=4

The above runs all sessions except the two very big ones: Flyspeck-Tame 
and JinjaThreads. Timing on 8 hyperthreaded Xeon cores:

   0:21:42 elapsed time, 3:34:29 cpu time, factor 9.88.

This means, almost all of AFP can be built in the same time as the "small" 
Isabelle examples that are part of the main repository! I did not expect 
that.  It means that AFP is not that big, or that the main repository is 
really bloated now.  (The reason why it all runs quite fast is that David 
Matthews is there in the background to make this insane multicore hardware 
usuable for us.)


The AFP editors should now take a look at the auto-generated configuration 
to see if they like it.  See also 
https://bitbucket.org/makarius/afp-build/src/a6ccf93b0574/NOTES for some 
fine points that have shown up in the inspection of the status-quo.

Note that generated theory sources are not supported by isabelle build -- 
it simply does not fit into the concept; this is no longer shell + make 
scripting.


 	Makarius