Isabelle

Release Candidates for Isabelle2025-1

The official Isabelle2025-1 release is scheduled for mid December 2025. This blog entry is dynamically updated to follow the sequence of public release candidates.

  • Isabelle2025-1-RC0 (07-Oct-2025): informal snapshot for experimentation, approx. 4 weeks before regular RC1. See also AFP/013063387a31.
  • Isabelle2025-1-RC1 (05-Nov-2025): first official release candidate, approx. 6 weeks before final lift-off. Almost everything is ready for testing; some documentation and add-on components still require updates. See also AFP/695d78dfa92a.
  • Isabelle2025-1-RC2 (19-Nov-2025): consolidated release candidate, ready for further testing and early applications. Some documentation still requires updates, and a few open problems remain. See also AFP/28b3dacf4cf9.
    Notable changes between RC1 and RC2:
    • Include Isabelle/Naproche component (with Intro.thy in the Documentation panel of Isabelle/jEdit).
    • Minor updates of a few Isabelle components: pdfjs, prismjs, sqlite, and jcef (omitted in the distribution).
    • Minor update of veriT executables: unchanged version, new arm64-darwin executable, rebuilt x64_84-darwin executable (macOS 12), replaced x86_64-windows executable (official download).
    • Isabelle/jEdit: more reactive mouse handling, notably on macOS.
    • Isabelle/jEdit: proper update of editor buffer syntax after defining new Isar commands.
    • Isabelle/jEdit: proper keycode names for LEFT, RIGHT, UP, DOWN.
    • Isabelle/jEdit: potentially more robust scrolling of initial session build progress.
    • Isabelle/VSCode: update of underlying vscodium component: version 1.105.17075 (September 2025).
    • Isabelle/VSCode: more robust session build process on console.
    • Isabelle/VSCode: command-line options “isabelle vscode -D property -J JAVAOPT”.
    • Isabelle/VSCode: more scalable support for theories that are loaded from the session database, e.g. HOL.List within Isabelle/HOL.
    • Isabelle/VSCode: avoid OCaml icons for Isabelle .ML files.
    • Isabelle/VSCode: uniform treatment of Isabelle symbols, using the static table provided at build time of the underlying vscodium component.
    • Isabelle/VSCode: fine-tuning of the underlying protocol wrt. Isabelle/Scala.
    • Isabelle/HOL: some clarification of command try0 with options try0_schedule and try0_default_timeout.
    • Isabelle/HOL: recover card_set code equation
    • Isabelle/HOL: minor library updates.
    • Isabelle/HOLCF: minor simproc update.
    • Isabelle/Scala: renamed “isabelle process” to “isabelle ML_process” to emphasize that it has been mostly superseded by “isabelle process_theories”, and avoid confusion with wording (“Isabelle process” refers to the Isabelle/Scala system process, not the Isabelle/ML runtime engine).
    • Isabelle/ML: Isabelle_Sytem.ML_process invokes “isabelle ML_process” directly from the running Isabelle/Scala process, without starting another Java Virtual Machine of the command-line tool.
    • Isabelle/Scala: more scalable output of JSON, e.g. for Isabelle/VSCode protocol.
    • Command-line tool “isabelle process_theories”: proper handling of console interrupts.
    • Update of Phabricator/Phorge server.
  • Isabelle2025-1-RC3 (01-Dec-2025): further consolidated release candidate, ready for final testing and regular applications. All known problems have been addressed. See also AFP/3af26ffddf1b.
    Notable changes between RC2 and RC3:
    • Proper PIDE markup for “theory … imports X Y Z”, relevant for Isabelle/jEdit, Isabelle/VSCode, HTML browser info.
    • Isabelle/jEdit: more robust mouse event handling, especially relevant for macOS with Magic Mouse. Avoid spurious text selection after jumping around in the editor (e.g. via hyperlinks).
    • Isabelle/jEdit: proper target offset when jumping to other buffers, e.g. in Documentation or Theories panel.
    • Isabelle/jEdit: update of doc jedit, new screenshots from macOS 26 using FlatLaF macOS Light.
    • Isabelle/VSCode: proper PIDE markup for semantic text color.
    • HOL: last-minute clarification of options for sledgehammer and try0.
    • HOL: last-minute changes to sessions HOL-Data_Structures and HOL-Library.
    • System: default Docker image is now based on ubuntu:24.04, instead of ubuntu:22.04.
  • Isabelle2025-1-RC4 (08-Dec-2025) with alternative download: pre-final release candidate, for even more testing and regular applications. See also the Archive of Formal Proofs.
    Notable changes between RC3 and RC4:
    • Poly/ML: update to version ccd3e3717f72 from branch fixes-5.9.2, which addresses a serious problem in the operation IntInf.~>> (right shift) – relevant for Isabelle/HOL code generation with SML target.
    • Isabelle/ML: redundant checks for IntInt.~>> to make double sure that it now works properly (to disappear before the final release).
    • Isabelle/jEdit: more reactive event handling for tree view in Output and Documentation, slightly different behaviour for Debugger (“Threads”).
    • Isabelle/jEdit: navigator records original position (mouse) before jumping via hyperlink.
    • Isabelle/VSCode: proper treatment of \<^bold> control symbol (editor view, symbols panel).
  • Isabelle2025-1 (17-Dec-2025): final release. See also the Archive of Formal Proofs.
    Final changes wrt. RC4:
    • Minor changes to doc isar-ref: more complete Index.
    • Isabelle/ML: omit redundant checks for IntInt.~>> (right shift).

The corresponding Mercurial repository clone is availabe via hg clone https://isabelle.sketis.net/repos/isabelle-release