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



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

Le 12/11/2021 à 21:26, Makarius a écrit :
Dear Isabelle users,

please see https://isabelle.sketis.net/website-Isabelle2021-1-RC3 and
https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1
for further progress on the release process.

There is now a proper download for Linux (ARM), and the "isabelle
build_docker" tools works for it (relevant on Apple M1 hardware).

This is also the fork-point of the isabelle-dev repository, which continues
for the time after this release:
https://isabelle.sketis.net/repos/isabelle/rev/4f1c1c7eb95f


Reminder: Any feedback about release candidates should be posted with a meaningful
Subject (not just a clone of the announcement).

We have approx. 4 weeks left until final lift-off: afterwards there will be no
more changes on this line.


	Makarius

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