Re: [isabelle] Isabelle2021-1-RC3 sledgehammer works fine on ARM64



Hello Makarius,

> So for Isabelle2021-1-RC1 nothing is going to happen --- unless you come up
> with a patch for z3-4.4.0 or z3-4.4.1 (based on the included one for 4.4.1).

I have compiled the old z3-4.4.0 a while ago for playing around with native arm64 Isabelle.
Luckily I just found my patches are still there, so I have attached them.
Iirc, in addition to very similar patches as you have done already, I just did a recursive sed replacing __in by __z3_in and __out by __z3_out.
It can be built like this:

CC=clang CXX=clang++ python scripts/mk_make.py && \
sed -i 's/-msse2//g' build/config.mk && \
sed -i 's/-msse//g' build/config.mk && \
sed -i 's/-mfpmath=sse//g' build/config.mk && \
cd build && \
make -j8

I didn’t bother messing around in their python build system code and instead just remove the x86-specific flags manually in the generated files.
At least this works for me on Gentoo/glibc.

In any case though...
> I've come to the conclusion
> that supporting z3 on arm64-linux requires a proper update to a current
> version https://github.com/Z3Prover/z3/tags
> 
> We cannot warp the underlying z3 several years from distant past into the
> present, without significant work on the Isabelle side.
I do agree on this in the long run. These are really just dirty hacks.

Florian

Attachment: 0001-arm64-patches.patch
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.