[isabelle-dev] Experimental support for arm64-linux

[Makarius]

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. I've purchased
that for a bit less than 100 EUR; a suitable micro SD storage card needs to be
added (e.g. 128 GB for 20 EUR).


The most relevant Isabelle components already include arm64-linux parts, but
jdk is still missing. This works e.g. via the Ubuntu package "openjdk-11-jdk"
and the following $ISABELLE_HOME_USER/etc/settings:

ISABELLE_JDK_HOME="/usr/lib/jvm/java-11-openjdk-arm64"

An alternative is to download/unpack JDK 11 from https://adoptopenjdk.net
(platform aarch64) and point to that directory. I will include that in the
next official update of the jdk component, probably at the end of October.


Now most Isabelle/Scala tools should work properly, as well as Isabelle/ML
based on the existing interpreter by David Matthews for that platform: it is
approx. 50-100 times slower than the standard code-generator for x86_64.

Consequently, "isabelle jedit" might require some hours to build the Scala
jars + ML logic image for HOL (while ZF only requires minutes). To reduce
heat, it might require to disable the display and run "isabelle build -b HOL"
first via ssh.

At this stage we can already use sledgehammer with prover "e", e.g. in
$ISABELLE_HOME/src/HOL/Metis_Examples/BigO.thy on many of the metis proofs.
This requires some patience, but it is fun to see it all work on this tiny
little device.


Overall the experiment is not just for fun: Apple might ship fancy new ARM
MacBooks within a few months.

So we need to think about collecting some money for David Mattews to produce a
proper code generator for Poly/ML eventually. People who have some ideas
should contact me or David via private mail.


	Makarius