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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
