Re: [isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'
Good points. I’ve added the slow/very_slow and x64 hints to the documentation now. Cheers, Gerwin > On 15.01.2018, at 07:38, Makariuswrote: > > 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 >> /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 > > Or: > > isabelle build -d '$AFP' -a -X very_slow -j4 > > You can also use -D '$AFP' (without -a) to address precisely the AFP > sessions. > > >> 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 > http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html > for typical maximum heap requirements. > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'
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 > /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 Or: isabelle build -d '$AFP' -a -X very_slow -j4 You can also use -D '$AFP' (without -a) to address precisely the AFP sessions. > 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 http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html for typical maximum heap requirements. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'
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 /doc/regression-test.md but that merely states the command. 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. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev