The official Isabelle2023 release is scheduled for early September 2023. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.

• Isabelle2023-RC0 (07-Jun-2023): informal snapshot for experimentation, approx. 4 weeks before regular RC1.

• Isabelle2023-RC1 (11-Jul-2023): first official release candidate, approx. 8 weeks before final lift-off. Almost everything is ready for testing. See also AFP/e2e58e494821.

• Isabelle2023-RC2 (26-Jul-2023): further consolidation of release candidate, now awaiting serious testing by users. See also AFP/1217567e2037. Notable changes since RC1:
  • The new isabelle profiling tool produces ML heap statistics.
  • The isabelle build tool now supports option -A to include AFP as directory.
  • Toplevel results (theorems etc.) are printed as regular writeln message instead of state.
  • More efficient specifications (in class): amending performance regression from Isabelle2022.
  • More refinements of specifications and proofs in session HOL-Analysis.
  • Isabelle/Scala: support for TOML (Tom's Obvious, Minimal Language).
  • Isabelle/Scala: more robust support for concurrent transactions in PostgreSQL.
  • Isabelle/Scala: beginning support for build cluster management, as collections of SSH hosts with shared PostgreSQL access.

• Isabelle2023-RC3 (10-Aug-2023): further consolidated release candidate and fork-point of the development repository. See also AFP/4605c928f00e. Notable changes since RC2:
  • Poly/ML: more robust support for ARM64 platform (native Apple Silicon).
  • PIDE: proper treatment of command keywords, notably for proof state output and parallel execution.
  • PIDE: proper treatment of previous theory for command print_theorems.
  • HOL: more robust support for corecursion.
  • HOL: refinement of lemma insert_Times_insert.
  • HOL-Analysis: more refinements of specifications and proofs.

• Isabelle2023-RC4 (27-Aug-2023): pre-final release candidate, after the fork point of afp-2023. Notable changes since RC3:
  • Last-minute improvement of Sledgehammer for vampire.
  • More scalable SQL database management, e.g. for session exports and distributed builds.
  • More robust support for distributed build clusters, including minimal documentation (status: experimental).
  • Proper Isar command print_context_tracing.

• Isabelle2023-RC5 (03-Sep-2023): one more release candidate, with notably last-minute tuning:
  • Update of Isabelle/Naproche: more examples (from "100 Theorems").
  • More portable $ISABELLE_HOSTNAME on Linux: trusty old hostname command is no longer required.
  • More robust $ISABELLE_TMP on Windows, outside of Cygwin root directory.
  • More robust SMT solver process management on Windows, notably for verit on Windows 11.
  • More robust support for distributed build clusters, including isabelle build_process -r -f to purge old database state.

• Isabelle2023 (11-Sep-2023): final version with minor additions to documentation:
  • jedit manual includes section "Build and view documents interactively"