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

[Fabian Immler]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190122/432e8523/attachment.bin>