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




> Am 15.11.2021 um 21:01 schrieb Makarius <makarius at sketis.net>:
> 
> On 15/11/2021 20:38, Florian Märkl wrote:
>> 
>>> 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.
> 
> Can you explain the purpose of __z3_in and __z3_out?

Just from a quick glance at the code I think they are just hints for the reader to mark function arguments as inputs or outputs.
They are defined to nothing and my assumption seems to match their usage. So they could essentially be removed entirely as well.

> I will try clang, but it takes all very long on this tiny Raspberrypi device.

The clang version I used, in case it helps:
clang version 12.0.1
Target: aarch64-unknown-linux-gnu
Thread model: posix
InstalledDir: /usr/lib/llvm/12/bin
Selected GCC installation: /usr/lib/gcc/aarch64-unknown-linux-gnu/11.1.0
Candidate multilib: .;@m64
Selected multilib: .;@m64

Florian



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