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



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




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