On 03/10/2020 16:43, Makarius wrote:
> Here is an intermediate report on the state of support for the ARM64 platform,
> according to Isabelle/694d0a315d0a.
>
> Presently, its main hardware representative is my new Raspberry Pi 4B (4 CPU
> cores at 1.5 GHz, 8 GB RAM), running Ubuntu Linux 20.04 LTS.
> This requires some patience, but it is fun to see it all work on this tiny
> little device.
Here are some timings for Isabelle/3e84f4e9651a on Pi OS 64bit beta (Debian
10.6):
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)
It is good to see that our huge HOL image already works on this tiny machine,
with interpreted Poly/ML.
HOL-Analysis and HOL-Library failed, due some to odd timeouts and missing z3
for arm64-linux.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
