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