[isabelle-dev] Proven support for Linux ARM64

[Makarius]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: z3.patch
Type: text/x-patch
Size: 2499 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240213/ab250b03/attachment.bin>