Recent Posts

View All

• Update/rebuild external provers on currently supported OS platforms, notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.

• An updated version of the veriT solver is now included as Isabelle component. It can be used in the smt proof method via smt (verit) or via declare [[smt_solver = verit]] in the context; see also session HOL-Word-SMT_Examples.

1. Document preparation ###

The next anticipated release is Isabelle2021 (February 2021). The hot phase with release candidates will presumably be 28-Dec-2020 .. 15-Feb-2020.

• Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session (instead of an external Java process): this improves reactivity and saves resources. This experimental feature is guarded by system option kodkod_scala (default: false).

• Isabelle server allows user-defined commands via isabelle_scala_service.

• The shell function isabelle_directory (within etc/settings of components) augments the list of special directories for persistent symbolic path names. This improves portability of heap images and session databases. It used to be hard-wired for Isabelle + AFP, but other projects may now participate on equal terms.

1. Isabelle/jEdit Prover IDE ###

• ML statistics via an external Poly/ML process: this allows monitoring the runtime system while the ML program sleeps.

• Theory_Data extend operation is obsolete and needs to be the identity function; merge should be conservative and not reset to the empty value. Subtle INCOMPATIBILITY and change of semantics (due to Theory.join_theory from Isabelle2020). Special extend/merge behaviour at the begin of a new theory can be achieved via Theory.at_begin.

• System option "pide_session" is enabled by default, notably for standard "isabelle build": it allows to invoke Isabelle/Scala operations from Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:

1. Isabelle/jEdit Prover IDE ###

1. Document preparation ###

• Isabelle/Phabricator setup has been updated to follow ongoing development: libphutil has been discontinued. Minor INCOMPATIBILITY: existing server installations should remove libphutil from /usr/local/bin/isabelle-phabricator-upgrade and each installation root directory (e.g. /var/www/phabricator-vcs/libphutil).

• The command-line tool "isabelle sessions" explores the structure of Isabelle sessions and prints result names in topological order (on stdout).

• The command-line tool isabelle build_docker has been slightly improved: it is now properly documented in the system manual.

• Mixfix annotations may use "' " (single quote followed by space) to separate delimiters (as documented in the isar-ref manual), without requiring an auxiliary empty block. A literal single quote needs to be escaped properly. Minor INCOMPATIBILITY.

1. Isabelle/jEdit Prover IDE ###

1. Isabelle/jEdit Prover IDE ###

The official Isabelle2020 release is scheduled for April 2020. This blog entry is dynamically updated to follow the sequence of public release candidates.

• The command-line tool "isabelle scala_project" creates a Gradle project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA.

The next anticipated release is Isabelle2020 (April 2020). The hot phase with release candidates will presumably be 01-Mar-2020 .. 15-Apr-2020.

• The command-line tool "isabelle hg_setup" simplifies the setup of Mercurial repositories, with hosting via Phabricator or SSH file server access.

• The command-line tool "isabelle phabricator_setup" facilitates self-hosting of the Phabricator software-development platform, with support for Git, Mercurial, Subversion repositories. This helps to avoid monoculture and to escape the gravity of centralized version control by Github and/or Bitbucket. For further documentation, see chapter "Phabricator server administration" in the "system" manual. A notable example installation is https://isabelle-dev.sketis.net/.