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



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




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