[isabelle-dev] Proven support for Linux ARM64
Makarius
makarius at sketis.net
Tue Feb 6 21:47:08 CET 2024
With Isabelle/37e57ac55559 we now have proven support for Linux ARM64, meaning
that there is a nightly "isabelle build -a" on a virtual server (from Netcup).
The Admin/build_release now works on Linux ARM64, and can produce logic images
for Linux ARM64. Thus regular repository snapshots (and release candidates)
support that platform by default, e.g. see
https://isatest.sketis.net/devel/release_snapshot
Still missing (to be investigated further) are the following external tools:
* z3: stuck at the rather old version 4.4.0, which lacks arm64-linux
binaries; the 4.4.1 arm64 package from ancient Debian is somewhat unstable on
current Ubuntu 20.04, see also failure of HOL-SMT_Examples recorded on
https://isatest.sketis.net/devel/build_status/index.html
* cvc4 (or rather cvc5)
* nunchaku
* smbc
* ocaml / opam
Makarius
More information about the isabelle-dev
mailing list