[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Jasmin Blanchette]

> What is special about Sudoku?

You're right, probably nothing.

>> SMT_Tests (requires Z3)
> ...
> In 2013 we did not have Z3 as default component, usable for everybody. Now the condition on it is always true -- z3 is always enabled.

We could indeed enable it by default.

>> Slow:
>> Brackin
>> IsaFoR
>> Misc_N2M
>> 
>> Probably also in the slow category (the last three might have a benchmarking component):
>> Find_Unused_Assms_Examples
>> Needham_Schroeder_No_Attacker_Example
>> Needham_Schroeder_Guided_Attacker_Example
>> Needham_Schroeder_Unguided_Attacker_Example
>> 
>> Slow and benchmarking:
>> Record_Benchmark
> 
> These are the genuine examples where I understand the arrangement as "test this continuously in the background, and record good performance figures for it".

I guess in that sense they are "Benchmarks". For "Brackin" etc., we were just interested in checking that they work at all -- and took them out when we saw that they were slow. But they do serve a dual purpose, esp. that "working at all" implies "not being *too* slow". So I won't object anymore to their characterization as "benchmarks".

Jasmin