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




Le 13/11/2021 à 18:33, David Matthews a écrit :
On 12/11/2021 21:43, Frédéric Boulanger wrote:
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.

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

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

--
Frédéric Boulanger
CentraleSupélec - Département Informatique	Laboratoire Méthodes Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex	Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 69 85 14 84


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