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



On 15/11/2021 21:01, Makarius wrote:
> 
> I did not try the alternative clang setup yet.
> 
> With the default gcc incantations, it all builds, but in the very end there is
> a final error:
> /usr/bin/ld: smt/smt.a(smt_statistics.o): Relocations in generic ELF (EM: 62)
> /usr/bin/ld: smt/smt.a(smt_statistics.o): Relocations in generic ELF (EM: 62)
> /usr/bin/ld: smt/smt.a(smt_statistics.o): Relocations in generic ELF (EM: 62)
> /usr/bin/ld: smt/smt.a: error adding symbols: file in wrong format
> collect2: error: ld returned 1 exit status
> make: *** [Makefile:3520: z3] Error 1
> 
> 
> I will try clang, but it takes all very long on this tiny Raspberrypi device.

This is all a bit tedious: my Pi OS installation lacks clang/clang++.

Luckily, there is an existing executable here:
https://packages.debian.org/stretch/arm64/z3/download

So I will just bundle the binaries as Isabelle component z3-4.4.1 and continue
with that --- so far it looks good.


	Makarius




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