Re: [isabelle] Isabelle2021-1-RC0 available for experiments


It would be nice to minimise incompatibilities with the previous version by adding:

abbreviation strict_sorted :: "'a::ord list ⇒ bool" where
  "strict_sorted ≡ sorted_wrt (<)"

to List.thy

I had no problem to fix the proofs that rely on strict_sorted with a call to sledgehammer.

On MacOS, the Isabelle2021-1-RC0 application does not behave as a regular MacOS application: you cannot drag a .thy file onto its icon or select "Open with..." to open a theory with it.

I wrote an Applescript application to fix this, it is available at:

I don't know how difficult it is to integrate this into the development of Isabelle. It amounts to processing OAPP and ODOC Apple Events.

I am very interested in the arm64 version because I prepare Docker images for my students with everything they need for my courses, and some of them have Apple Silicon M1 computers this year. Thanks for making this happen!

Best regards,

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

Le 3 oct. 2021 à 21:03, Makarius <makarius at> a écrit :

Dear Isabelle users,

the next release is scheduled for 15-Dec-2021 (or a bit earlier). The first
official release candidate will appear around 01-Nov-2021.

To warm up, here is a informal snapshot for experimentation and early

Many things are still missing: for example there will be a proper linux-arm
distribution eventually, e.g. for docker on Apple Silicon M1.

Many other things are already there, but not yet covered in NEWS.


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