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/ && \
sed -i 's/-msse2//g' build/ && \
sed -i 's/-msse//g' build/ && \
sed -i 's/-mfpmath=sse//g' build/ && \
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
> 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.


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

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