[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