On Sun, 31 Jan 2016, Lars Hupel wrote:
The "ISABELLE_FULL_TEST" variable and "slow" group are somehow adhoc
measures to get meaningful interactive tests, without wasting too much
time. It probably makes sense to imitate that for "testboard" setups.
The idea is to distribute the build load over multiple machines, since
that isn't supported by "isabelle build". This is generally helpful –
even if we get better hardware – because distributing jobs is trivial
with Jenkins and there's no reason we shouldn't. The shorter the build
time, the better.
Some years ago we were in a similar situation of outdated hardware, and
Isabelle + AFP sessions growing beyond feasibility. So we started to
speculate towards distributed "make".
When Isabelle "build" took over in 2012, the multicore support of Poly/ML
+ Isabelle/ML was already so advanced that the question was irrelevant.
A full test of Isabelle + AFP required less than 1h on a plain and basic
2 * 4 core machine (macbroy2).
Now we have much bigger Isabelle + AFP sessions, and still the same old
hardware.
Clustering weak nodes always requires more administrative efforts than
just one or two fat nodes without special tricks.
Building with SML/NJ configuration is trivial. It would be "just another
job" in Jenkins. I'd just need to know about what to build precisely.
Can you explain to me what the ML_SYSTEM_POLYML variable means?
I full hypersearch over Isabelle + AFP confirms that the documentation in
the "system" manual is still correct:
\<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is
\<^verbatim>\<open>true\<close> for @{setting ML_SYSTEM} values derived
from Poly/ML, as opposed to SML/NJ where it is empty. This is
particularly useful with the build option @{system_option condition}
(\secref{sec:system-options}) to restrict big sessions to something that
SML/NJ can still handle.
Concerning what "SML/NJ can still handle", see also
https://bitbucket.org/isabelle_project/isabelle-release/commits/a4e6ea45f416
That commit is only on the isabelle-release repository. It will come back
via merge in something like 2 weeks.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
