HomeIsabelle/Phabricator
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).
  • Isabelle2021-RC4 (01-Feb-2021): pre-final release candidate; see also AFP. Notable changes:
    • Bundling of Naproche-SAD with Prover IDE support for .ftl and .ftl.tex files; see also $ISABELLE_NAPROCHE/Ex.thy in the Isabelle/jEdit Documentation panel.
    • Application bundle on macOS supports security dialogs to access special user directories: Desktop, Documents, Downloads.
    • Directory layout of macOS application bundle follows Linux, with more direct access to command-line tool wrapper Isabelle2021-RC4.app/bin/isabelle.
    • Slightly more parallelism in HTML presentation.
    • More robust HTML output: treat remaining conflicts of \<^bsub> ... \<^esub> with semantic markup.
    • More robust signature annotations in Isabelle/Haskell: support experimental haskell-stack-trace-plugin.
    • Update to latest Java 15.0.2 (Jan-2021).
    • Follow Phabricator update 2021 Week 4.
  • Isabelle2021-RC5 (08-Feb-2021): presumably last release candidate; see also AFP. Notable changes:
    • Improved support for Apple Silicon (ARM): external processes are managed by Isabelle/Scala instead of Apple's Rosetta (which does not support multithreaded process fork).
    • Isabelle/jEdit: update to latest flatlaf-1.0rc3.
    • Isabelle/jEdit: avoid conflict of options for Metal GUI fonts with FlatLaf.
    • Isabelle/jEdit: open external viewer for hyperlinks to certain file-formats (PDF etc.).
    • Update of Isabelle/Naproche component: improved examples.
  • Isabelle2021-RC6 (14-Feb-2021): the very last release candidate; see also AFP. Notable changes:
    • More robust interrupts for Isabelle_System.bash (ML via Scala) on Apple Silicon.
    • Update to flatlaf-1.0 GUI look-and-feel.
    • Update of Isabelle/Naproche component: improved examples and documentation.
Written by makarius on Nov 30 2020, 1:15 PM.
User
Projects
None
Subscribers
None

Event Timeline