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