> On 02.02.2016, at 08:28, Lars Hupel <hu...@in.tum.de> wrote: > >> What remains are various benchmarks. We could move these sessions to >> ~~/src/Benchmarks and omit that directory in ~~/ROOTS. Thus it can be >> included on demand like this: >> >> isabelle build -d '~~/src/Benchmarks' -a >> >> or like this: >> >> isabelle build -D '~~/src/Benchmarks' >> >> This avoids more sophisticated Boolean algebra on session groups. It >> also makes clear from the source structure, what is normally not tested. >> >> I basically do the same with -d '$AFP' all the time. > > Sounds reasonable. There's no pressure to do it just yet; I'd be happy > to wait for post-release mode.
I have a slight worry concerning the characterization and naming as "benchmarks". From what I understand, a "benchmark" is a theory file that tests the performance of the system. Looking at the list 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 I would say that only "Record_Benchmark" is truly benchmarking. The others are merely slow examples or examples that require a special setup. Special setup: Sudoku SMT_Tests (requires Z3) 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 Conversely, some examples that are always processed can be considered benchmarking -- e.g. "Nitpick_Examples/Hotel_Nits.thy". Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
