Release Candidates for Isabelle2021

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

  • Isabelle2021-RC0 (30-Nov-2020): informal snapshot for experimentation, approx. 4 weeks before regular RC1.
  • Isabelle2021-RC1 (27-Dec-2020): first official release candidate, approx. 7 weeks before final lift-off. Almost everything is ready for testing. See also AFP/7b26d4cc3c17.
  • Isabelle2021-RC2 (10-Jan-2020): consolidated release candidate and fork-point of isabelle-release vs. isabelle development repositories; see also AFP/03248eeafe63. Notable changes:
    • More portable Isabelle app bundling on Linux + macOS.
    • Update to Java 15, with native support for ARM64 (Apple Silicon).
    • Improved Isabelle/jEdit look-and-feel: portable and scalable FlatLAF on all platforms.
    • Improved Isabelle/jEdit action toggle-full-screen (overrides existing action).
    • More robust sledgehammer / cvc4 support.
    • More scalable HTML presentation: improved XML caching and hash-consing.
    • More complete PIDE markup in HTML presentation.
    • Various Isabelle/HOL library updates: sessions HOL, HOL-Library, HOL-Computational_Algebra, HOL-Complex_Analysis, HOL-Data_Structures
  • Isabelle2021-RC3 (24-Jan-2020): further consolidated release candidate; see also AFP/eb0cc2599588. Notable changes:
    • Update to current scala-2.13.4: requires changes to Isabelle/HOL code generator concerning ArraySeq.
    • Isabelle/jEdit: improved support for macOS 11.1 Big Sur full-screen mode.
    • Isabelle/jEdit: hypesearch results are docked by default, for more robustness concerning window managers and full-screen mode (notably macOS Big Sur).
    • Isabelle/jEdit: proper heap free status for JVM.
    • Minor update of Isabelle/jEdit documentation: screenshots on macOS Big Sur with FlatLaf look-and-feel.
    • Isabelle/jEdit: update to latest flatlaf-1.0rc1.
    • More robust HTML output: avoid conflict of \<^bsub> ... \<^esub> with semantic markup.
    • Proper semantic completion for @{cite ...} document antiquotations.
    • Formal update of Isabelle/VSCode: proper Isabelle2021 extension available on VSCode market place.
    • More Isabelle/Scala and Isabelle/Haskell operations for TCP servers.
    • Update to current GHC stack lts-16.31.
    • Command-line tool isabelle components has new options -u and -x.
    • Clarified return code of isabelle build timeout: 142 = 128 + 14 (SIGALRM), instead of interrupt (130) or error (1).
Written by makarius on Nov 30 2020, 1:15 PM.

Event Timeline