Monthly Archives: October 2025

Isabelle, Science

Invited talk at Malinca Kickoff-Meeting in Paris

I have attended the Malinca project Kickoff-Meeting from 01..03-Oct-2025, and delivered an invited talk about Human-readable Proof Documents and Embedded Sublanguages in Isabelle/Isar.

Abtract:

Isabelle/Pure was originally introduced by Paulson (1986/1989) as a Logical Framework to specify object-logics declaratively, based on Higher-order Natural Deduction. Isabelle/HOL emerged soon as main object-logic and Isabelle application, with many tools for specifications and proofs written in Isabelle/ML.

Isabelle/Isar was added by Wenzel (1999) as a structured language for Human-readable formal proof documents: it works with Isabelle/Pure and regular object-logics. The proof language has been reworked over the decades, with notable extensions in 2015/2016, including the Eisbach language for Isar Proof Methods. Already, from the beginning, Isar had been accompanied by the Isabelle Document language, to write mathematical texts with high-quality typesetting in LaTeX.

So today we may see Isabelle as an agglomeration of many languages for different purposes, all integrated into a single System Framework in Isabelle/Scala. That includes the Isabelle/PIDE Prover IDE with parallel and asynchronous processing of formal documents, and the Isabelle build system (with its distributed cluster manager). Thus we can carry the weight and gravity of large proof documents, as e.g. seen in the Archive of Formal Proofs (AFP).

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