[isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

Makarius makarius at sketis.net
Sun Jan 14 21:38:09 CET 2018

On 14/01/18 12:42, Clemens Ballarin wrote:
> Dear Maintainers of Isabelle / the AFP,
> Where would I find instructions on actually getting 'isabelle afp_build
> -A' to run through?  I was hoping to find that in
> <afp-devel>/doc/regression-test.md but that merely states the command.

My command-line usually looks like this:

  isabelle build -d '$AFP' -a -X slow -j4


  isabelle build -d '$AFP' -a -X very_slow -j4

You can also use -D '$AFP' (without -a) to address precisely the AFP

> It appears that I would need to set ML_PLATFORM=x86_64-darwin for the
> large sessions but then some magic seems to defeat that and builds are
> still for x86-darwin.

Instead of editing $ISABELLE_HOME_USER/etc/settings to change
ML_PLATFORM (which is difficult to get right), I usually edit
$ISABELLE_HOME_USER/etc/preferences to add:

  ML_system_64 = true

Only some "slow" sessions do need x86_64, but some non-slow sessions
(like HOL-ODE-Numerics) become a bit slow in x86 mode. Almost everything
else works better in x86 mode, which is the default.

See also
for typical maximum heap requirements.


More information about the isabelle-dev mailing list