Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-1-RC3 sledgehammer works fine on ...


view this post on Zulip Email Gateway (Nov 12 2021 at 21:44):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Hello,

I just installed the RC3 release for arm64 in a Docker container running
on an Apple M1 chip, and the issues I had with sledgehammer in RC1 seem
to be fixed.

It works fine and provides better proofs than in Isabelle2021 on an
Intel chip.

Many thanks for this!

The MacOS version works fine on both Intel and M1 machines, but I wonder
if it takes advantage of the M1 chip. It is shown as an Intel
application on both platforms, but I see arm64-darwin directories in the
packaged polyml-5.9 and jdk-17 distributions, so the support for the M1
chip may be quite good although the NEWS file let me think that the
Intel version of Poly/ML is still used through Rosetta 2.

Frédéric

view this post on Zulip Email Gateway (Nov 12 2021 at 22:07):

From: Makarius <makarius@sketis.net>
On 12/11/2021 22:43, Frédéric Boulanger wrote:

I just installed the RC3 release for arm64 in a Docker container running on an
Apple M1 chip, and the issues I had with sledgehammer in RC1 seem to be fixed.

It works fine and provides better proofs than in Isabelle2021 on an Intel chip.

Many thanks for this!

Great. The thanks need to be directed towards David Matthews, who is refining
Poly/ML 5.9 towards a release where ARM will work natively (on Linux, macOS,
Windows), but be still somewhat inefficiently due to lack of code optimization.

The MacOS version works fine on both Intel and M1 machines, but I wonder if it
takes advantage of the M1 chip. It is shown as an Intel application on both
platforms, but I see arm64-darwin directories in the packaged polyml-5.9 and
jdk-17 distributions, so the support for the M1 chip may be quite good
although the NEWS file let me think that the Intel version of Poly/ML is still
used through Rosetta 2.

I have already built many components for arm64-linux, and a few for
arm64-darwin (external provers etc.).

Java 15 in Isabelle2021 has already been native arm64-darwin, and this
continues with Java 17 in Isabelle2021-1.

In contrast, the native Poly/ML arm64_32-darwin (and arm64-darwin) is only
there for testing, to sort out remaining problems. On macOS, x86_64_32-darwin
performs much better with Rosetta 2 and will remain the default for now.

You can try ARM by augmenting $ISABELLE_HOME_USER/etc/settings like this:

ML_PLATFORM="arm64_32-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"

This will build an image for Isabelle/HOL on startup of Isabelle/jEdit.

Makarius

view this post on Zulip Email Gateway (Nov 13 2021 at 17:33):

From: David Matthews <dm@prolingua.co.uk>
I'm pleased it works well for you. The ARM64 port involves quite a few
components. The focus so far has been on getting the essential parts
working, tested and fixing bugs. Register optimisation isn't critical
so that has been left for the moment. As a result the ARM64 port
doesn't perform quite as well as the X86 version with Rosetta.
Hopefully that will change when there has been time to work on optimisation.

David

view this post on Zulip Email Gateway (Nov 13 2021 at 21:05):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Thank you for the explanations, and the good work!

I provide my students with a Docker image containing all the software
they need for the year, and some of them have MacBooks with M1 chips so
they need the arm64-linux version of the image.

I did not make extensive tests and only checked that what I need for my
courses works. I also managed to build the Why3 <http://why3.lri.fr/>
Isabelle session in which many proofs "by smt" failed with RC1, so I
guess it is all the interface with smt solvers that benefits from the
work on Poly/ML.

Frédéric

view this post on Zulip Email Gateway (Nov 15 2021 at 18:37):

From: Makarius <makarius@sketis.net>
Poly/ML on arm64 is one thing, and external provers are another thing. I have
successfully built most tools for arm64-linux, with the following exceptions:

. cvc4
. z3
. nunchaku
. smbc

The default for the "smt" proof method is z3, but veriT is getting more and
more significant, which is already on arm64-linux.

After spending many hours with z3-4.4.0 and z3-4.4.1, which are both quite old
but close to our current component z3-4.4.0pre-3, 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.

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).

Makarius
a.patch

view this post on Zulip Email Gateway (Nov 15 2021 at 19:38):

From: Florian Märkl <isabelle-users@florianmaerkl.de>
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
0001-arm64-patches.patch

view this post on Zulip Email Gateway (Nov 15 2021 at 20:01):

From: Makarius <makarius@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?

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

view this post on Zulip Email Gateway (Nov 15 2021 at 20:15):

From: Florian Märkl <isabelle-users@florianmaerkl.de>

Am 15.11.2021 um 21:01 schrieb Makarius <makarius@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

view this post on Zulip Email Gateway (Nov 15 2021 at 21:46):

From: Makarius <makarius@sketis.net>
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


Last updated: Jul 15 2022 at 23:21 UTC