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



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?


> 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 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:

ontend.o shell/main.o shell/mem_initializer.o shell/smtlib_frontend.o
shell/gparams_register_modules.o api/api.a opt/opt.a parsers/smt/smtparser.a
tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.a
tactic/ufbv/ufbv_tactic.a tactic/fpa/fpa_tactics.a
tactic/smtlogics/smtlogic_tactics.a tactic/nlsat_smt/nlsat_smt_tactic.a
muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a
muz/tab/tab.a muz/clp/clp.a muz/pdr/pdr.a muz/rel/rel.a
muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a
duality/duality.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a
tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a
smt/proto_model/proto_model.a smt/params/smt_params.a
ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a
ast/macros/macros.a ast/fpa/fpa.a ast/simplifier/simplifier.a
ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a
cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a
solver/solver.a tactic/aig/aig_tactic.a
math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a
tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a
tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a
parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a
model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a
ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a
math/interval/interval.a math/simplex/simplex.a math/hilbert/hilbert.a
nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a  -lpthread
-fopenmp -lrt
/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.


	Makarius




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