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.)
- Projects
- None
- Subscribers
- None