[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Makarius]

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:
>
> HOL-ex
>    Sudoku
> HOL-Datatype_Examples
>    Brackin
>    IsaFoR
>    Misc_N2M
> HOL-Word-SMT_Examples
>    SMT_Tests
> HOL-Quickcheck_Benchmark
>    Find_Unused_Assms_Examples
>    Needham_Schroeder_No_Attacker_Example
>    Needham_Schroeder_Guided_Attacker_Example
>    Needham_Schroeder_Unguided_Attacker_Example
> HOL-Record_Benchmark
>    Record_Benchmark
>
> 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 
for SML/NJ.

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?


 	Makarius