Release Candidates for Isabelle2023

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"
Written by makarius on Jun 7 2023, 4:24 PM.

Event Timeline