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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
