Release Candidates for Isabelle2021-1

The official Isabelle2021-1 release is scheduled for December 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.

  • Isabelle2021-1-RC0 (03-Oct-2021): informal snapshot for experimentation, approx. 4 weeks before regular RC1.
  • Isabelle2021-1-RC1 (01-Nov-2021): first official release candidate, approx. 6 weeks before final lift-off. Almost everything is ready for testing. See also AFP/b40b44b920f5.
  • Isabelle2021-1-RC2 (07-Nov-2021): consolidated release candidate. See also AFP/3a75f572994c. Notable changes:
    • HTML presentation now includes links to formal entities.
    • Improved page breaks of Documentation main.
    • Update of veriT component: more robust treatment of timeout signals.
    • Update of Poly/ML pre-5.9 test version: more robust support for ARM platform.
    • isabelle scala_project now uses Maven instead of Gradle (less ambitious, more stable)
    • More accurate jEdit sources: allow to build Isabelle/Scala project via Maven, or within the Java/Scala IDE that operates on the Maven project.
  • Isabelle2021-1-RC3 (12-Nov-2021): further consolidated release candidate and fork-point of the development repository. See also AFP/e5eeaaf2bd5b. Notable changes:
    • Update of Poly/ML pre-5.9 test version: more robust support for ARM platform, with Isabelle application bundle on website.
    • MinitSat now works properly on Windows (for Nitpick).
    • More robust "isabelle mirabelle" tool: proper output via Isabelle/Scala export artifacts.
    • isabelle build_docker now works properly without perl, and for linux_arm.
    • Minor update of isabelle_setup component: it requires Java 15 for isabelle scala_project.
    • New option document_echo (more verbosity).
    • Minor additions to HOL libraries.
    • Pro-forma update of Isabelle/VSCode extension
  • Isabelle2021-1-RC4 (26-Nov-2021): pre-final release candidate, after fork-point of AFP. Notable changes:
    • Update to official Poly/ML 5.9 release.
    • More robust support for veriT SMT solver.
    • Update to Java Swing FlatLAF 1.6.4.
    • Partial support for Z3 on arm64-linux (e.g. relevant for docker on Apple Silicon M1).
    • More robust Nitpick/Kodkod: uniform use of external (bulky) Java process for better interrupts (option kodkod_scala = false).
    • More robust standard argument for system options, e.g. isabelle build -o document -o document_output instead of isabelle build -o document=pdf -o document_output=output.
    • Options document_heading_prefix and document_comment_latex support Dagstuhl LIPIcs.
    • Isar presentation commands (like section, text etc.) define LaTeX output in Isabelle/ML, with XML markup that is interpreted in Isabelle/Scala (class Latex.Output). See also theory Pure-ex.Alternative_Headings.
    • More robust and scalable HTML presentation.
    • Last-minute changes to HOL-Analysis.
  • Isabelle2021-1-RC5 (04-Dec-2021): presumably the last release candidate, before final release within 10 days. Notable changes:
    • quickcheck and try are back to physical timeout (situation before Isabelle2019): this works better with massive heap allocations, as GC time is included in the measurement.
    • Updated documentation: implementation and system.
    • Admin/build_release works without auxiliary Java 11.
    • Include updated version of Isabelle/Naproche component, with lots of new examples. (Very few examples are presented here.)
Written by makarius on Nov 1 2021, 4:48 PM.

Event Timeline