Email Gateway (Nov 05 2025 at 18:36): Email Gateway (Nov 05 2025 at 18:36):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
this calendar year has two Isabelle releases (which happen every 8-10 months).
We are now ready to start the release process for Isabelle2025-1 (December
2025). See also the continuously updated blog post
https://sketis.net/2025/release-candidates-for-isabelle2025-1
The current release candidate is available from
https://isabelle.in.tum.de/website-Isabelle2025-1-RC1
A corresponding version of the Archive of Formal Proofs is
https://isabelle.sketis.net/repos/afp-devel/rev/695d78dfa92a
The NEWS and ANNOUNCE files are already up-to-date, but some documentation
still requires update.
The coming weeks are dedicated to thorough testing of release candidates.
Afterwards the release will become final and unchangeable as usual.
Any feedback about Isabelle release candidates should be posted with a
meaningful Mail subject, not just a clone of this announcement.
Makarius
Email Gateway (Nov 07 2025 at 10:54):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius, dear all,
first, thank you Makarius for taking care of the roll-out of Isabelle 2025-1.
Second, here is short report from the IsaFoR side.
Adaptation of IsaFoR from Isabelle 2025 to Isabelle 2025-RC 1 was quite smooth.
However, there is a small problems that I recently encountered, which might be fixed before the
release of 2025-1: SML-export does result in Code that does not compile using SML New Jersey:
theory Scratch imports Main
begin
definition "f x = (x = True)"
export_code f in SML
end
results in the upcoming SML-code:
fun equal_bool p true = p
| equal_bool p false = not p
| equal_bool true p = p
| equal_bool false p = not p;
This code is refused by the New Jersey SML compiler, as the last two equations can never be applied.
The code-equations for equality on bool (code_thms f) should in my opinion be
reduced to only two of them (either 2-3 or 4-5).
(1) equal_class.equal ?p ?p ≡ True
(2) equal_class.equal ?p True ≡ ?p
(3) equal_class.equal ?p False ≡ ¬ ?p
(4) equal_class.equal True ?p ≡ ?p
(5) equal_class.equal False ?p ≡ ¬ ?p
Best,
René
Am 05.11.2025 um 19:36 schrieb Makarius <makarius@sketis.net>:
Dear Isabelle users,
this calendar year has two Isabelle releases (which happen every 8-10 months). We are now ready to start the release process for Isabelle2025-1 (December 2025). See also the continuously updated blog post https://sketis.net/2025/release-candidates-for-isabelle2025-1
The current release candidate is available from https://isabelle.in.tum.de/website-Isabelle2025-1-RC1
A corresponding version of the Archive of Formal Proofs is https://isabelle.sketis.net/repos/afp-devel/rev/695d78dfa92a
The NEWS and ANNOUNCE files are already up-to-date, but some documentation still requires update.
The coming weeks are dedicated to thorough testing of release candidates. Afterwards the release will become final and unchangeable as usual.
Any feedback about Isabelle release candidates should be posted with a meaningful Mail subject, not just a clone of this announcement.
Makarius
Last updated: Nov 09 2025 at 20:21 UTC