[isabelle-dev] Grouping ISABELLE_FULL_TEST?
jasmin.blanchette at inria.fr
Thu Feb 4 05:16:59 CET 2016
> 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.
>> Probably also in the slow category (the last three might have a benchmarking component):
>> Slow and benchmarking:
> 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".
More information about the isabelle-dev