[isabelle-dev] Proven support for Linux ARM64

[Jasmin Blanchette]

Hi Makarius,

> 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

See my previous email.

>  * cvc4 (or rather cvc5)

CVC4 would be nice to have, but it's not critical in the same way as Z3.

cvc5 used to crash on Mac, but I'm told by Clark Barrett that with version 1.1.0 they've solved many Mac-specific bugs. I can experiment with it on my Mac and if it seems to work well, we could upgrade to that.

>  * nunchaku
> 
>  * smbc

Nunchaku (and its backend SMBC) never left the experimental stage. Maybe we could move them out of "HOL" and mark them more clearly as experimental? I haven't given up all hopes of developing Nunchaku further and indeed just this week I was talking with a candidate about doing this, but it shouldn't block Isabelle releases.

>  * ocaml / opam

Thankfully somebody else's concern. :)

Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9337
Email: jasmin.blanchette at ifi.lmu.de
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 6. Feb 2024, at 21:47, Makarius <makarius at sketis.net> wrote:
> 
> 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
> 
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240214/ac9ef4f9/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4674 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240214/ac9ef4f9/attachment-0001.bin>