[isabelle-dev] Proven support for Linux ARM64

[Jasmin Blanchette]

Hi Makarius,

Thanks for investigating this. The binary components are always a special source of worry.

From what I understand, HOL-SMT_Examples will continue working thanks to the certificate caching mechanism that is used there. The mechanism isn't used in the AFP, though, which means arm64-linux users won't be able to load many AFP entries due to "smt" calls to Z3 in there. If this is too much of an issue, we could consider either of two solutions:

1. Replace the "smt" calls. Most of them could use the "(verit)" option instead, and for the others, we'd have to come up with alternative proofs. This possibly entails a lot of work, but it could be done by a "task force".

2. Use certificates for the AFP (and require their use in the future). Certificates take the form of low-level (SMT input, SMT output) pairs, so that when "smt" generates a given SMT input in the cache, the SMT output is used directly instead of running the SMT solver.

Best,
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 13. Feb 2024, at 12:36, Makarius <makarius at sketis.net> wrote:
> 
> On 06/02/2024 21:47, Makarius 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).
>> 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
> 
> I've spent a lot of time experimenting with z3 4.4.0pre (0482e7fe727c), but did not succeed so far (as of Isabelle/6e5f40cfa877): The session HOL-SMT_Examples fails with timeout, due to non-terminating invocations of z3 on arm64-linux.
> 
> For verit there was a similar problem, but rebuilding it from source (with "docker run -it ubuntu:18.04 bash") made it work; see also see Isabelle/b14c4cb37d99.
> 
> 
> For z3 the build instructions are as follows, using the attached z3.patch, which is based on the Debian package and changes found in the z3 repository:
> 
> """
> docker run -it ubuntu:16.04 bash
> apt-get update && apt-get upgrade -y && apt autoremove -y
> apt install -y curl less libfontconfig1 libgomp1 openssh-client perl pwgen rlwrap make g++ python
> 
> mkdir z3-4.4.0pre
> cd z3-4.4.0pre
> curl --location https://github.com/Z3Prover/z3/archive/0482e7fe727c.tar.gz | tar --strip-components=1 -xz -f -
> 
> #inline z3.patch below
> patch -p1 <<EOF
> ...
> EOF
> 
> python scripts/mk_make.py
> cd build && make
> """
> 
> 
> That is minor progress, because the build works at all, by using ubuntu:16.04 instead of our official ubuntu:18.04 baseline.
> 
> For the planned release of Isabelle2024 (May 2024), I tend to disable z3 on arm64-linux by default (via etc/settings of the component), and no longer pretend that we have something working, see also https://isabelle-dev.sketis.net/rISABELLE796ae338eb9d
> 
> 
> 	Makarius
> <z3.patch>_______________________________________________
> 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/c6e012f3/attachment.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/c6e012f3/attachment.bin>