These numbers look quite extreme:The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as it seems to be the case with polyml-test-0a6ebca445fc).
The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0: ML_PLATFORM="x86-linux" ML_OPTIONS="--minheap 2000 --maxheap 4000"Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time, factor 2.66) Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time, factor 1.46)
ML_PLATFORM="x86_64-linux" ML_OPTIONS="--minheap 2000 --maxheap 4000"Finished HOL-ODE-Numerics (0:29:34 elapsed time, 1:21:08 cpu time, factor 2.74) Finished HOL-ODE-ARCH-COMP (0:06:49 elapsed time, 0:12:41 cpu time, factor 1.86)
Fabian On 1/22/2019 11:36 AM, Makarius wrote:
On 19/01/2019 21:43, Makarius wrote:Thanks to great work by David Matthews, there is now an Isabelle component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" It requires the usual "isabelle components -a" incantation afterwards.polyml-test-0a6ebca445fc is the default in 81ca77cb7c8c, it means the scope of further testing has widened. Almost everything has become faster by default, but an exception are heavy-duty int computations that rely on a certain word size, notably the HOL-ODE family of sessions. AFP/a04825886e71 marks various sessions explicitly as "large", which means that they prefer x86_64. Here are concrete numbers: x86_64_32-linux -minheap 1500 Finished Pure (0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00) Finished HOL (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45) Finished HOL-Analysis (0:03:48 elapsed time, 0:21:27 cpu time, factor 5.64) Finished Ordinary_Differential_Equations (0:01:14 elapsed time, 0:05:31 cpu time, factor 4.43) Finished Differential_Dynamic_Logic (0:01:29 elapsed time, 0:05:03 cpu time, factor 3.39) Finished HOL-ODE-Numerics (0:17:51 elapsed time, 0:46:30 cpu time, factor 2.60) Finished Lorenz_Approximation (0:04:02 elapsed time, 0:07:46 cpu time, factor 1.92) Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10) Finished HOL-ODE-ARCH-COMP (0:12:56 elapsed time, 0:28:35 cpu time, factor 2.21) Finished HOL-ODE-Examples (0:37:13 elapsed time, 2:51:00 cpu time, factor 4.59) Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44) x86_64-linux --minheap 3000 Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 1.00) Finished HOL (0:02:44 elapsed time, 0:09:28 cpu time, factor 3.47) Finished HOL-Analysis (0:04:05 elapsed time, 0:22:47 cpu time, factor 5.58) Finished Ordinary_Differential_Equations (0:01:19 elapsed time, 0:05:49 cpu time, factor 4.40) Finished Differential_Dynamic_Logic (0:01:33 elapsed time, 0:05:22 cpu time, factor 3.44) Finished HOL-ODE-Numerics (0:18:59 elapsed time, 0:49:00 cpu time, factor 2.58) Finished Lorenz_Approximation (0:04:01 elapsed time, 0:07:39 cpu time, factor 1.90) Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.20) Finished HOL-ODE-ARCH-COMP (0:04:06 elapsed time, 0:08:37 cpu time, factor 2.10) Finished HOL-ODE-Examples (0:05:18 elapsed time, 0:17:04 cpu time, factor 3.22) Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
