Saw this at https://isabelle.in.tum.de/dist/Isabelle2021/doc/NEWS.html
Is there any way I can help test the arm64-linux platform build?
Experimental means that it works for Makarius.
The issue is that PolyML does not support compilation on those platforms. The code is only interpreted, making it order of magnitude too slow be useful (at least as a user of the PIDE interface)
Oh and Makarius is not here on zulip
PolyML is available on my debian-arm distro. Is that not build from source?
It is available and works. It just a lot slower
Basically: you give polyml code. Then either you can choose between the slow and the first version (like on x86), or you have only the slow version (like ARM)
Finished Pure (0:07:01 elapsed time, 0:07:01 cpu time, factor 1.00) Finished HOL (3:04:18 elapsed time, 8:52:18 cpu time, factor 2.89) Finished HOL-Word (0:28:07 elapsed time, 1:33:39 cpu time, factor 3.33) Finished HOLCF (0:11:18 elapsed time, 0:26:53 cpu time, factor 2.38)
Ok. Thanks for the link.
To quote the PolyML download page https://www.polyml.org/download.html:
Please note: although Poly/ML is released as source the source actually contains binary versions of the compiler. There are native code versions for i386 and x86-64. The configure script will select the appropriate version. On other architectures it will use interpreted byte code which will necessarily be slower than the native code versions.
My machine is much faster than a raspberry, but not more than 30 times as fast:
Finished Pure (0:00:18 elapsed time, 0:00:17 cpu time, factor 0.95) Finished HOL (0:04:55 elapsed time, 0:13:45 cpu time, factor 2.79) Finished HOLCF (0:00:23 elapsed time, 0:00:50 cpu time, factor 2.16)
I see. Thanks.
Last updated: Dec 07 2023 at 08:19 UTC