[isabelle-dev] Grouping ISABELLE_FULL_TEST?
makarius at sketis.net
Sun Jan 31 14:41:57 CET 2016
On Sun, 31 Jan 2016, Lars Hupel wrote:
> As of 527488dc8b90, there are five sessions which contain theories that
> are only processed under ISABELLE_FULL_TEST=true:
> Most of these appear to be benchmarks of some sort. Currently, the new
> CI setup doesn't set the ISABELLE_FULL_TEST flag. I think it would be
> useful to run those, but I'd like to split them up into a separate run
> so that they can be executed in parallel to the regular makeall. To that
> end, I would suggest grouping these sessions in 'full'. I could then run
> export ISABELLE_FULL_TEST=true
> isabelle build -v -g full
> (In a similar fashion, I run 'slow' sessions separately from the others.)
We have accumulated a fair amount of complication here. There was a time
when it was even more complication, but we managed to recover from it by
substantial improvements of Poly/ML (multithreading and parallel GC),
elimination of "make", and introduction of up-to-date hardware.
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.
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.
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
Or we could discontinue SML/NJ altogether. I proposed that the last time
10 years ago.
Here are also the canonical meta questions:
* What is really required?
* What is the simplest way to achieve that?
* What can be discontinued?
More information about the isabelle-dev