HomeIsabelle/Phabricator
Phame Blogs Isabelle NEWS
Isabelle NEWS
History of user-relevant changes

Demo documents for well-known LaTeX styles

Written by makarius on Nov 2 2022, 1:28 PM.
  1. Document preparation ###
Read more...

Zstd compression for Isabelle/Scala and Isabelle/ML

Written by makarius on Oct 21 2022, 7:50 PM.
  • Operations for Zstd compression (via Isabelle/Scala):
Read more...

MLton compiler for x86_64-linux

Written by makarius on Sep 17 2022, 11:40 PM.
  • The MLton compiler for x86_64-linux has been bundled as Isabelle component, since Ubuntu 22.04 no longer provides a suitable package. Note that on macOS, MLton is readily available via Homebrew: https://formulae.brew.sh/formula/mlton
Read more...

Isabelle/Scala SSH connections use OpenSSH executables

Written by makarius on Sep 15 2022, 11:55 AM.
  • Isabelle/Scala SSH connections now use regular OpenSSH executables from the local system: ssh, scp, sftp; the old ssh-java component has been discontinued. This has various practical consequences:
Read more...

Command-line tool "isabelle log" and option "show_states"

Written by makarius on Sep 9 2022, 4:15 PM.
  • Command-line tool isabelle log has been refined to support multiple sessions, and to match messages against regular expressions (using Java Pattern syntax).
Read more...

Display of schematic goal instance

Written by makarius on Sep 9 2022, 4:05 PM.
  • The instantiation of schematic goals is now displayed explicitly as a list of variable assignments. This works for proof state output, and at the end of a toplevel proof. In rare situations, a proof command or proof method may violate the intended goal discipline, by not producing an instance of the original goal, but there is only a warning, no hard error.
Read more...

Session ROOT files support 'chapter_definition' entries

Written by makarius on Aug 27 2022, 10:08 PM.
  • Old-style {* verbatim *} tokens have been discontinued (legacy feature since Isabelle2019). INCOMPATIBILITY, use ‹cartouche› syntax instead.
Read more...

System: Isabelle/Scala is now based on Scala 3

Written by makarius on Jul 6 2022, 5:14 PM.
Read more...

Isabelle/ML type Bytes.T and XZ compression

Written by makarius on Jul 6 2022, 3:38 PM.
  • Type Bytes.T supports scalable byte strings, beyond the limit of String.maxSize (approx. 64 MB on 64_32 architecture).
Read more...

Command-line tools "isabelle hg_sync" and "isabelle sync"

Written by makarius on Jun 11 2022, 11:01 PM.
  • Command-line tool isabelle hg_sync synchronizes the working directory of a local Mercurial repository with a target directory, using rsync notation for destinations.
Read more...

Isabelle/VSCode as bundled application

Written by makarius on Mar 25 2022, 1:37 PM.
  1. Isabelle/VSCode Prover IDE ###
Read more...

ML antiquotation "instantiate"

Written by makarius on Oct 28 2021, 9:50 PM.
  • ML antiquotation "instantiate" allows to instantiate formal entities (types, terms, theorems) with values given ML. This works uniformly for "typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the instantiation. A mode "(schematic)" behind the keyword means that some variables may remain uninstantiated (fixed in the specification and schematic in the result); by default, all variables need to be instantiated.
Read more...

More robust (and more strict) treatment of abstractions within the context

Written by makarius on Oct 19 2021, 9:46 PM.
  • Term operations under abstractions are now more robust (and more strict) by using the formal proof context in subsequent operations:
Read more...

Nitpick with external/portable MiniSat

Written by makarius on Oct 8 2021, 11:25 AM.
  • Nitpick: External solver "MiniSat" is available for all supported Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only works for Intel Linux and macOS.
Read more...

Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"

Written by makarius on Sep 27 2021, 5:00 PM.
  • The improper proof command guess is no longer part of by Pure, but provided by the separate theory Pure-ex.Guess. INCOMPATIBILITY, existing applications need to import session Pure-ex and theory Pure-ex.Guess. Afterwards it is usually better eliminate the guess command, using explicit obtain instead.
Read more...

ML antiquotations for object-logic judgement

Written by makarius on Sep 22 2021, 12:52 PM.
  • ML antiquotations make_judgment and dest_judgment refer to corresponding functions for the object-logic of the ML compilation context. This supersedes older mk_Trueprop / dest_Trueprop operations.
Read more...

ML antiquotations for type constructors and term constants

Written by makarius on Sep 22 2021, 12:17 PM.
  • ML antiquotations for type constructors and term constants:
Read more...

Isabelle/ML "build" combinators

Written by makarius on Sep 22 2021, 12:11 PM.
  • The build combinators of various data structures help to build content from bottom-up, by applying an add function the empty value. For example:
Read more...

Scalable operations for Thm.instantiate and Thm.generalize

Written by makarius on Sep 22 2021, 12:08 PM.
  • ML structures TFrees, TVars, Frees, Vars, Names provide scalable operations to accumulate items from types and terms, using a fast syntactic order. The original order of occurrences may be recovered as well, e.g. via TFrees.list_set.
Read more...

Configuration option "show_results"

Written by makarius on Sep 22 2021, 12:04 PM.
  • Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled in interactive mode, but it could occasionally cause unnecessary slowdown. It can be disabled like this:
Read more...

Bundles for lattice syntax

Written by makarius on Sep 22 2021, 12:01 PM.
  • Theory HOL-Library.Lattice_Syntax has been superseded by bundle lattice_syntax: it can be used in a local context via include or in a global theory via unbundle. The opposite declarations are bundled as no_lattice_syntax. Minor INCOMPATIBILITY.
Read more...

Localized commands 'syntax' and 'no_syntax'

Written by makarius on Sep 22 2021, 11:57 AM.
  • Commands syntax and no_syntax now work in a local theory context, but there is no proper way to refer to local entities --- in contrast to notation and no_notation. Local syntax works well with bundle, e.g. see lattice_syntax vs. no_lattice_syntax in theory Main of Isabelle/HOL.
Read more...

Isabelle/Scala improvements

Written by makarius on Jul 18 2021, 10:16 PM.
  • Each Isabelle component may specify a Scala/Java jar module declaratively via etc/build.props (file names are relative to the component directory). E.g. see $ISABELLE_HOME/etc/build.props with further explanations in the system manual.
Read more...

Reactivated ML profiling

Written by makarius on Jun 9 2021, 12:11 PM.
  • ML profiling has been updated and reactivated, after some degration in

Isabelle2021:

Read more...

More predefined Isabelle symbols

Written by makarius on Jun 7 2021, 2:56 PM.
  • More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit.
Read more...

System options short form (e.g. "-o document")

Written by makarius on Jun 7 2021, 2:45 PM.
  • System option system_log specifies an optional log file for internal messages produced by Output.system_message in Isabelle/ML; the value true refers to console progress of the build job. This works for isabelle build or any derivative of it.
Read more...

High-quality blackboard-bold symbols

Written by makarius on Mar 21 2021, 11:58 PM.
  1. Document preparation ###
Read more...

Remote provers from SystemOnTPTP via Isabelle/Scala

Written by makarius on Mar 14 2021, 10:11 PM.
Read more...

Improved LaTeX typesetting of ‹...›

Written by makarius on Mar 11 2021, 11:24 AM.
  1. Document preparation ###
Read more...

Clarified timeouts for Isabelle/ML tools

Written by makarius on Mar 5 2021, 10:29 PM.
  • 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.
Read more...

External bash processes are always managed by Isabelle/Scala

Written by makarius on Feb 23 2021, 12:13 AM.
  • External bash processes are always managed by Isabelle/Scala, in contrast to Isabelle2021 where this was only done for macOS on Apple Silicon.
Read more...

Improved GUI look-and-feel

Written by makarius on Jan 9 2021, 1:20 AM.
  1. Isabelle/jEdit Prover IDE ###
Read more...

Isabelle/jEdit action "isabelle.goto-entity"

Written by makarius on Dec 18 2020, 11:38 AM.
  1. Isabelle/jEdit Prover IDE ###
Read more...

Message logs from session build database

Written by makarius on Dec 11 2020, 12:09 AM.
  • 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.
Read more...

Document antiquotation for Isabelle tools

Written by makarius on Nov 30 2020, 1:09 PM.
  1. Document preparation ###
Read more...

PDF/HTML presentation in Isabelle/Scala, based on session build database

Written by makarius on Nov 21 2020, 7:49 PM.
  • 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.
Read more...

Experimental support for arm64-linux platform

Written by makarius on Oct 26 2020, 9:42 PM.
  • Experimental support for arm64-linux platform. The reference platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
Read more...

Update external prover components for Sledgehammer etc.

Written by makarius on Oct 19 2020, 5:02 PM.
  • Update/rebuild external provers on currently supported OS platforms, notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
Read more...

Include veriT component for "smt" method

Written by makarius on Oct 19 2020, 4:59 PM.
  • 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.
Read more...

Document preparation engine updates

Written by makarius on Sep 27 2020, 9:21 PM.
  1. Document preparation ###
Read more...

Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session

Written by makarius on Aug 25 2020, 3:44 PM.
  • 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).
Read more...

User-defined Isabelle server commands via isabelle_scala_service

Written by makarius on Aug 17 2020, 7:07 PM.
  • Isabelle server allows user-defined commands via isabelle_scala_service.
Read more...

More systematic support for special directories

Written by makarius on Aug 17 2020, 7:05 PM.
  • 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.
Read more...

Improved monitoring for Isabelle/ML and Java

Written by makarius on Aug 13 2020, 4:22 PM.
  1. Isabelle/jEdit Prover IDE ###
Read more...

ML statistics via an external Poly/ML process

Written by makarius on Aug 7 2020, 11:33 PM.
  • ML statistics via an external Poly/ML process: this allows monitoring the runtime system while the ML program sleeps.
Read more...

Theory_Data extend operation is obsolete and needs to be the identity function

Written by makarius on Jul 20 2020, 11:59 PM.
  • 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.
Read more...

System option pide_session is enabled by default

Written by makarius on Jun 17 2020, 9:55 PM.
  • 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:
Read more...

Update of Isabelle/jEdit to jedit-5.6pre1

Written by makarius on Jun 11 2020, 2:57 PM.
  1. Isabelle/jEdit Prover IDE ###
Read more...

Antiquotations for Isabelle systems programming

Written by makarius on May 27 2020, 4:44 PM.
  1. Document preparation ###
Read more...

Update of Isabelle/Phabricator setup

Written by makarius on May 18 2020, 5:08 PM.
  • 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).
Read more...

Command-line tool "isabelle sessions"

Written by makarius on Apr 28 2020, 10:16 PM.
  • The command-line tool "isabelle sessions" explores the structure of Isabelle sessions and prints result names in topological order (on stdout).
Read more...

Slightly improved isabelle build_docker tool

Written by makarius on Mar 21 2020, 10:42 PM.
  • The command-line tool isabelle build_docker has been slightly improved: it is now properly documented in the system manual.
Read more...

Mixfix annotations may use single-quote-space as documented

Written by makarius on Mar 15 2020, 1:48 PM.
  • 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.
Read more...

Support Java/VM monitoring via jconsole

Written by makarius on Mar 6 2020, 8:45 PM.
  1. Isabelle/jEdit Prover IDE ###
Read more...

Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions

Written by makarius on Mar 2 2020, 3:44 PM.
  1. Isabelle/jEdit Prover IDE ###
Read more...

Command-line tool "isabelle scala_project"

Written by makarius on Jan 15 2020, 3:34 PM.
  • The command-line tool "isabelle scala_project" creates a Gradle project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA.
Read more...

Command-line tool "isabelle hg_setup"

Written by makarius on Dec 19 2019, 8:43 PM.
  • The command-line tool "isabelle hg_setup" simplifies the setup of Mercurial repositories, with hosting via Phabricator or SSH file server access.
Read more...

Isabelle/Phabricator setup

Written by makarius on Dec 16 2019, 9:28 PM.
  • 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/.
Read more...
About Isabelle NEWS

This blog publishes Isabelle/NEWS items as they emerge in the isabelle-dev process. Official Isabelle releases only contain the final version of it as NEWS file in the toplevel directory.