[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Makarius]

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