Stream: General

Topic: Raspberry Pi OS

William Mitchell (Apr 17 2021 at 15:59):

Saw this at https://isabelle.in.tum.de/dist/Isabelle2021/doc/NEWS.html

• Experimental support for arm64-linux platform. The reference platform
  is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).

Is there any way I can help test the arm64-linux platform build?

Mathias Fleury (Apr 17 2021 at 16:03):

Experimental means that it works for Makarius.

Mathias Fleury (Apr 17 2021 at 16:05):

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)

Mathias Fleury (Apr 17 2021 at 16:06):

Oh and Makarius is not here on zulip

William Mitchell (Apr 17 2021 at 16:16):

PolyML is available on my debian-arm distro. Is that not build from source?

Mathias Fleury (Apr 17 2021 at 16:17):

It is available and works. It just a lot slower

Mathias Fleury (Apr 17 2021 at 16:19):

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)

Mathias Fleury (Apr 17 2021 at 16:21):

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)

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2020-October/017254.html

William Mitchell (Apr 17 2021 at 16:23):

Ok. Thanks for the link.

Mathias Fleury (Apr 17 2021 at 16:28):

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.

Mathias Fleury (Apr 17 2021 at 16:30):

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)

William Mitchell (Apr 17 2021 at 16:33):

I see. Thanks.

Last updated: Apr 25 2024 at 04:18 UTC