[isabelle-dev] HOL-ODE-Numerics vs. HOL-ODE-Refinement

[Makarius]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: HOL-ODE-Numerics_timing.png
Type: image/png
Size: 5832 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180531/9356647d/attachment.png>