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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
