High-quality blackboard-bold symbols
Written by makarius on Sun, Mar 21, 11:58 PM in Isabelle NEWS.
- Document preparation ###
Remote provers from SystemOnTPTP via Isabelle/Scala
Written by makarius on Sun, Mar 14, 10:11 PM in Isabelle NEWS.
- Remote provers from SystemOnTPTP (notably for Sledgehammer) are now managed via Isabelle/Scala instead of perl; the dependency on libwww-perl has been eliminated (notably on Linux). Rare INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
Improved LaTeX typesetting of ‹...›
Written by makarius on Mar 11 2021, 11:24 AM in Isabelle NEWS.
- Document preparation ###
Clarified timeouts for Isabelle/ML tools
Written by makarius on Mar 5 2021, 10:29 PM in Isabelle NEWS.
- Timeouts for Isabelle/ML tools are subject to system option timeout_scale --- this already used for the overall session build process before, and allows to adapt to slow machines. The underlying Timeout.apply in Isabelle/ML treats an original timeout specification 0 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY in boundary cases.
External bash processes are always managed by Isabelle/Scala
Written by makarius on Feb 23 2021, 12:13 AM in Isabelle NEWS.
- External bash processes are always managed by Isabelle/Scala, in contrast to Isabelle2021 where this was only done for macOS on Apple Silicon.
Improved GUI look-and-feel
Written by makarius on Jan 9 2021, 1:20 AM in Isabelle NEWS.
- Isabelle/jEdit Prover IDE ###
Isabelle/jEdit action "isabelle.goto-entity"
Written by makarius on Dec 18 2020, 11:38 AM in Isabelle NEWS.
- Isabelle/jEdit Prover IDE ###
Message logs from session build database
Written by makarius on Dec 11 2020, 12:09 AM in Isabelle NEWS.
- The command-line tool isabelle log prints prover messages from the build database of the given session, following the the order of theory sources, instead of erratic parallel evaluation. Consequently, the session log file is restricted to system messages of the overall build process, and thus becomes more informative.
Release Candidates for Isabelle2021
Written by makarius on Nov 30 2020, 1:15 PM in Isabelle Release.
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.
Document antiquotation for Isabelle tools
Written by makarius on Nov 30 2020, 1:09 PM in Isabelle NEWS.
- Document preparation ###
PDF/HTML presentation in Isabelle/Scala, based on session build database
Written by makarius on Nov 21 2020, 7:49 PM in Isabelle NEWS.
- The command-line tool isabelle build provides option -P DIR to produce PDF/HTML presentation in the specified directory; -P: refers to the standard directory according to ISABELLE_BROWSER_INFO / ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken from the build database -- from this or earlier builds with option document=pdf.
Experimental support for arm64-linux platform
Written by makarius on Oct 26 2020, 9:42 PM in Isabelle NEWS.
- Experimental support for arm64-linux platform. The reference platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
Update external prover components for Sledgehammer etc.
Written by makarius on Oct 19 2020, 5:02 PM in Isabelle NEWS.
- Update/rebuild external provers on currently supported OS platforms, notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
Include veriT component for "smt" method
Written by makarius on Oct 19 2020, 4:59 PM in Isabelle NEWS.
- 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.
Document preparation engine updates
Written by makarius on Sep 27 2020, 9:21 PM in Isabelle NEWS.
- Document preparation ###
Plan for Isabelle2021 release
Written by makarius on Sep 25 2020, 4:13 PM in Isabelle Release.
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
Written by makarius on Aug 25 2020, 3:44 PM in Isabelle NEWS.
- 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).
User-defined Isabelle server commands via isabelle_scala_service
Written by makarius on Aug 17 2020, 7:07 PM in Isabelle NEWS.
- Isabelle server allows user-defined commands via isabelle_scala_service.
More systematic support for special directories
Written by makarius on Aug 17 2020, 7:05 PM in Isabelle NEWS.
- 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.
Improved monitoring for Isabelle/ML and Java
Written by makarius on Aug 13 2020, 4:22 PM in Isabelle NEWS.
- Isabelle/jEdit Prover IDE ###
ML statistics via an external Poly/ML process
Written by makarius on Aug 7 2020, 11:33 PM in Isabelle NEWS.
- 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
Written by makarius on Jul 20 2020, 11:59 PM in Isabelle NEWS.
- 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
Written by makarius on Jun 17 2020, 9:55 PM in Isabelle NEWS.
- 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:
Update of Isabelle/jEdit to jedit-5.6pre1
Written by makarius on Jun 11 2020, 2:57 PM in Isabelle NEWS.
- Isabelle/jEdit Prover IDE ###
Antiquotations for Isabelle systems programming
Written by makarius on May 27 2020, 4:44 PM in Isabelle NEWS.
- Document preparation ###
Update of Isabelle/Phabricator setup
Written by makarius on May 18 2020, 5:08 PM in Isabelle NEWS.
- 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).
Command-line tool "isabelle sessions"
Written by makarius on Apr 28 2020, 10:16 PM in Isabelle NEWS.
- The command-line tool "isabelle sessions" explores the structure of Isabelle sessions and prints result names in topological order (on stdout).
Slightly improved isabelle build_docker tool
Written by makarius on Mar 21 2020, 10:42 PM in Isabelle NEWS.
- 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-space as documented
Written by makarius on Mar 15 2020, 1:48 PM in Isabelle NEWS.
- 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.
Support Java/VM monitoring via jconsole
Written by makarius on Mar 6 2020, 8:45 PM in Isabelle NEWS.
- Isabelle/jEdit Prover IDE ###
Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions
Written by makarius on Mar 2 2020, 3:44 PM in Isabelle NEWS.
- Isabelle/jEdit Prover IDE ###
Release Candidates for Isabelle2020
Written by makarius on Feb 14 2020, 9:43 PM in Isabelle Release.
The official Isabelle2020 release is scheduled for April 2020. This blog entry is dynamically updated to follow the sequence of public release candidates.
Command-line tool "isabelle scala_project"
Written by makarius on Jan 15 2020, 3:34 PM in Isabelle NEWS.
- The command-line tool "isabelle scala_project" creates a Gradle project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA.
Plan for Isabelle2020 release
Written by makarius on Dec 22 2019, 6:08 PM in Isabelle Release.
The next anticipated release is Isabelle2020 (April 2020). The hot phase with release candidates will presumably be 01-Mar-2020 .. 15-Apr-2020.
Command-line tool "isabelle hg_setup"
Written by makarius on Dec 19 2019, 8:43 PM in Isabelle NEWS.
- The command-line tool "isabelle hg_setup" simplifies the setup of Mercurial repositories, with hosting via Phabricator or SSH file server access.
Isabelle/Phabricator setup
Written by makarius on Dec 16 2019, 9:28 PM in Isabelle NEWS.
- 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/.