[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Lars Hupel]

> 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.

> For regular batch tests in the style of "isatest", the main purpose is
> to accumulate accurate timing information, and preserve that in a simple
> format over a long time.  This has been forgotten in recent years, since
> measurements have become more and more messed up.  So performance-wise, we
> are flying blind, especially for AFP.

I can't yet say with confidence that we now have a setup with reliable
performance numbers. In a couple of days I will look at the numbers to
get an idea of their variance.

> A related question is what to do with SML/NJ and the ML_SYSTEM_POLYML
> variable.  For the Isabelle2016 release, I've tried to build everything
> with SML/NJ as usual, but many sessions failed, even just HOL-Library.
> 
> We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session
> for SML/NJ.
> 
> Or we could discontinue SML/NJ altogether.  I proposed that the last
> time 10 years ago.

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?

Cheers
Lars