HomeIsabelle/Phabricator
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.
Written by makarius on Feb 14 2020, 9:43 PM.
User
Projects
None
Subscribers
None

Event Timeline