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

Makarius makarius at sketis.net
Tue Jan 22 20:28:36 CET 2019


On 22/01/2019 20:05, Fabian Immler wrote:
> 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)

Can you point to some smaller parts of these sessions, where the effect
is visible? We can then use profiling to get an idea what actually
happens in x86_64_32.


	Makarius




More information about the isabelle-dev mailing list