Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Isabelle2025-2 supersedes Isabelle2025-1

Email Gateway (Jan 19 2026 at 11:39):

From: Makarius <makarius@sketis.net>

Due to a notable confusion of options for isabelle build, the release of
Isabelle2025-1 (December 2025) had to be replaced on the spot by
Isabelle2025-2 (January 2026).

The relevant NEWS entries are as follows:

* General *

• Command 'sorry' is rejected by "isabelle build" as expected, with the
  default option "quick_and_dirty=false". This was broken in
  Isabelle2025-1: Isar commands were considered interactive due to the
  default option "show_results=true". Proper behaviour could be recovered
  in Isabelle2025-1 via "isabelle build -o show_results=false", but it is
  better to use Isabelle2025-2. Both approaches result in minor changes of
  result messages stored in session build databases.

* Isabelle/jEdit Prover IDE *

• Console/Scala: proper treatment of interrupts via "Stop" button. It
  was broken since Isabelle2022: Scala interpreter thread became
  inoperative afterwards.

This refers to Isabelle/89701cf1768e.

The release website requires some time to be fully updated, including all
mirrors. Afterwards, I will make a proper announcement on isabelle-users.

The plan for Isabelle2026 (October 2026) remains unchanged:
https://sketis.net/2025/plan-for-isabelle2026-october-2026 --- thus we have
sufficient distance to the Christmas vacation.

The last time we've had the awkward situation to have one release supersede
another was Isabelle2013-2:
https://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/NEWS ---
there were many more posthoc changes, and I was really worried about the
overall state of affairs.

We have recovered from that pretty well in 2014/2015 by removing old system
variations that no longer had a purpose (TTY REPL and Proof General Emacs),
and by relying more on Isabelle/Scala than the somewhat accidental
operating-system environment.

Abstractly, the same idea is still relevant: this time it will be the removal
of the remains of ML-toplevel build (use_thy), together with odd historic
options like "interactive mode" for Isar commands. Regular system options are
sufficient (module Options in Isabelle/ML and Isabelle/Scala).

Makarius

Last updated: Feb 04 2026 at 02:22 UTC