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
