Release Candidates for Isabelle2020
The official Isabelle2020 release is scheduled for April 2020. This blog entry is dynamically updated to follow the sequence of public release candidates.
- Isabelle2020-RC0 (14-Feb-2020): informal snapshot for experimentation, a few weeks before regular RC1.
- Isabelle2020-RC1 (02-Mar-2020): first official release candidate, approx. 6 weeks before final lift-off. Almost everything is ready for testing. See also AFP/b8e1eebb4b17.
- Isabelle2020-RC2 (15-Mar-2020): consolidated release candidate and fork-point of isabelle-release vs. isabelle development repositories; see also AFP/23d7d61fa263. Notable changes:
- More robust output of proof terms with hidden polymorphism.
- Clarified notion of errors for Isabelle/jEdit navigation actions.
- More adequate default font sizes in Isabelle/jEdit for Linux on HD / UHD displays.
- New Isabelle/jEdit action isabelle.jconsole for Java/VM monitoring.
- Isabelle/jEdit formally requires Java 11, obsolete Java 8 no longer works.
- Full jEdit sources for "isabelle scala_project" Gradle project, for more convenient browsing in IntelliJ IDEA.
- Proper support of "' " (single quote followed by space) in mixfix annotations as documented since Feb-1995.
- Minor tuning of theories and proofs in Isabelle/HOL.
- More scalable YXML output in Isabelle/Scala.
- Pro-forma update of E prover component: rebuild on Linux and Windows.
- Isabelle2020-RC3 (23-Mar-2020): even more consolidated release candidate; see also AFP. Notable changes:
- Minor updates to documentation: isar-ref, jedit, system.
- Clarified notion of errors for Isabelle/jEdit navigation actions (again).
- Clarified default for antialiased text, with better performance especially on Linux.
- Avoid font problems on Windows with OpenJDK 10.0.6: back to 10.0.5.
- Update of Cygwin (Windows): slightly more robust setup (e.g. binutils).
- Proper treatment of base session in isabelle update: avoid updating its sources.
- Slightly improved isabelle build_docker tool, with proper documentation in system manual.
- Avoid duplication of messages in isabelle build.
- More robust treatment of ISABELLE_TMP_PREFIX in headless server, e.g. Isabelle/VSCode language server.
- More robust errors for thm_deps and thm_oracles.
- More robust naming of locale interpretations in session ZF-Constructible.
- Isabelle2020-RC4 (02-Apr-2020): pre-final release candidate; see also AFP. Notable changes:
- More robust output of proof terms with hidden polymorphism.
- More robust treatment of temporary files for nitpick.
- More informative messages for isabelle dump.
- Isabelle2020-RC5 (08-Apr-2020): pre-final release candidate; see also AFP. Notable changes:
- Proper support for sledgehammer with cvc4.
- Projects
- None
- Subscribers
- None