<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi Makarius,<div><br></div><div><blockquote type="cite">Still missing (to be investigated further) are the following external tools:<br><br> * 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<br></blockquote><div><br></div><div>See my previous email.</div><br><blockquote type="cite"> * cvc4 (or rather cvc5)</blockquote><div><br></div><div>CVC4 would be nice to have, but it's not critical in the same way as Z3.</div><div><br></div><div>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.</div><br><blockquote type="cite"> * nunchaku<br><br> * smbc<br></blockquote><div><br></div><div>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.</div><br><blockquote type="cite"> * ocaml / opam<br></blockquote><div><br></div>Thankfully somebody else's concern. :)</div><div><br></div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science and Theorem Proving<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9337<br>Email: jasmin.blanchette@ifi.lmu.de<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 6. Feb 2024, at 21:47, Makarius <makarius@sketis.net> wrote:</div><br class="Apple-interchange-newline"><div><div>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).<br><br><br>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<br><br><br><br><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br></div></div></blockquote></div><br></div></body></html>