[isabelle-dev] Experimental support for arm64-linux

[Makarius]

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