[isabelle-dev] Poly/ML x86_64_32 available for testing

[Makarius]

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