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