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.) If nobody complains, I'll add the group. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev