The session HOL-ODE-Numerics has become much slower recently (Isabelle/3a7f257dcac7:23e12da0866c and AFP/4b06a8701616:cf739ca5383b), but it seems be just a consequence of removing HOL-ODE-Refinement:
lxcisa0 threads=1 ML_PLATFORM="x86_64-linux" ML_HOME="/home/isabelle/contrib/polyml-5.7.1-5/x86_64-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="--minheap 4G --maxheap 32G" Isabelle/3a7f257dcac7, AFP/4b06a8701616 Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95) Finished HOL (0:06:56 elapsed time, 0:06:52 cpu time, factor 0.99) Finished HOL-Analysis (0:19:35 elapsed time, 0:19:34 cpu time, factor 1.00) Finished Ordinary_Differential_Equations (0:05:15 elapsed time, 0:05:14 cpu time, factor 1.00) Finished HOL-ODE (0:00:01 elapsed time) Finished HOL-ODE-Refinement (0:12:47 elapsed time, 0:14:12 cpu time, factor 1.11) Finished HOL-ODE-Numerics (0:32:22 elapsed time, 0:32:23 cpu time, factor 1.00) Isabelle/23e12da0866c, AFP/cf739ca5383b Finished Pure (0:00:17 elapsed time, 0:00:16 cpu time, factor 0.95) Finished HOL (0:06:54 elapsed time, 0:06:50 cpu time, factor 0.99) Finished HOL-Analysis (0:19:21 elapsed time, 0:19:20 cpu time, factor 1.00) Finished Ordinary_Differential_Equations (0:05:10 elapsed time, 0:05:09 cpu time, factor 1.00) Finished HOL-ODE-Numerics (0:43:08 elapsed time, 0:44:39 cpu time, factor 1.03) See also AFP/cf739ca5383b: user: immler date: Thu May 24 15:01:56 2018 +0200 files: metadata/metadata thys/Differential_Dynamic_Logic/ROOT thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy thys/Ordinary_Differential_Equations/Numerics/Refine_Vector_List.thy thys/Ordinary_Differential_Equations/ROOT thys/Ordinary_Differential_Equations/document/root.tex description: fewer auxiliary sessions for Ordinary_Differential_Equations I've required some time-consuming manual tests to get so that point. At first I was actually looking at the wrong spot: changeset: 68260:61188c781cdd user: haftmann date: Thu May 24 09:18:29 2018 +0200 files: NEWS src/HOL/Divides.thy src/HOL/Hoare_Parallel/RG_Examples.thy src/HOL/Library/Stream.thy src/HOL/ex/Parallel_Example.thy description: avoid overaggressive classical rule Before that change, HOL-ODE-Numerics was not terminating over brief history interval. This is an indication that the test infrastructure is still somewhat lacking: there should be an automated job to measure out an interval of changesets. Moreover, the status page https://isabelle.sketis.net/devel/build_status probably needs a formal record, where reasons and non-reasons for slowdowns can be documented and/or discussed. Anyway, with approx. 100min CPU time HOL-ODE-Numerics has become eligible for the "AFP slow" category: paradoxically this will make the test much faster, but also less accurate in its timing information, because the test hardware and settings are quite different. Makarius
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
