Re: [isabelle] Isabelle2021-1-RC3 sledgehammer works fine on ARM64
On 12/11/2021 21: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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and