Category Archives: Isabelle

MMT as component for Isabelle2019

MMT is a language, system and library (in Scala) to represent a broad range of languages in the OMDoc format: this supports formal, informal, semi-formal content. The MMT repository includes
general APIs to operate on OMDoc theories, together with various tools and applications. There are several MMT sub-projects to connect to other systems. This includes Isabelle/MMT, which appeared as preliminary version already in Nov-2018.

The release of Isabelle2019 (June 2019) is an opportunity to distribute MMT version 17.0.0 (May 2019) as Isabelle application. An alternative is to incorporate the underlying Isabelle component manually into Isabelle2019 in $ISABELLE_HOME_USER/etc/settings like this: init_component ".../mmt-20190611" — where the three dots refer to the directory where the component tar.gz has been unpacked.

In either case, the mmt.jar of the MMT distribution is included in the Isabelle/Scala package name space. The component provides Isabelle command-line tools as follows:

  • isabelle mmt_build to (re)build the MMT project inside the Isabelle system environment (only required after change of the Scala sources)
  • isabelle mmt_import to import the content of a headless Isabelle/PIDE session into MMT (OMDoc and RDF/XML triples)
  • isabelle mmt_server to present imported content using the built-in HTTP server of MMT
  • isabelle mmt to run the interactive MMT shell inside the Isabelle system environment, e.g. for experimentation within the Isabelle + MMT package namespace, using the scala sub-shell.

The main functionality is provided by isabelle mmt_import: that is a medium-sized Scala module (57KB) within the MMT code-base (file src/mmt-isabelle/src/info/kwarc/mmt/isabelle/Importer.scala). It refers to general export facilities of Isabelle/Scala, which are part of the Isabelle2019 distribution (file src/Pure/Thy/export_theory.scala). The latter may be studied independently of MMT in the implementation of the isabelle dump tool (file src/Pure/Tools/dump.scala); see also the Isabelle System Manual, section 2.6.

The following papers provide further explanations on Isabelle/MMT:

Isabelle/Naproche for Automatic Proof-Checking of Ordinary Mathematical Texts

Naproche-SAD is a recent tool by Frerix and Koepke, based on the original System for Automated Deduction (SAD) by Paskevich and others. It processes the Formal Theory Language (ForTheL), which is designed to look like mathematical text, but it is restricted to a small subset of natural language.

The tool is implemented in Haskell as a plain function from input text to output messages. A file is like a chapter of mathematical text, with a nested tree-structure of elements and sub-elements (for signatures, axiomatizations, statements, proofs). Output messages inform about the translation of mathematical text to problems of first-order logic, and indicate success or failure of external proof checking; the latter is delegated to the E Prover by Stephan Schulz and can take several seconds for each proof obligation.

To integrate Naproche-SAD into PIDE, Frerix and Wenzel have reworked the Haskell program over 2 months in 2018, to turn the command-line tool into a service for reactive checking of ForTheL texts. Isabelle integration was done via the new Isabelle/Haskell library and some glue code in Isabelle/Scala to register ForTheL as auxiliary file-format (extension .ftl).

[Isabelle/Naproche screenshot]

The resulting Isabelle/Naproche application is available as multi-platform download. A running instance is shown in the screenshot: users can directly open ForTheL files (e.g. from Documentation / Examples) and wait briefly to see output messages attached to the text in the usual IDE manner. Further edits produce a new version of the text, which is sent in total to Naproche-SAD again. The back-end is sufficiently smart to avoid redundant checking of unchanged sub-elements: it keeps a global state with results of old versions: this is easy to implement as the program keeps running until shutdown of Isabelle/PIDE.

(Cited from section 1.2 of the paper Interaction with Formal Mathematical Documents in Isabelle/PIDE.)

Isabelle presentations at LSV Paris/Cachan

During the two weeks of 17..28-Jun-2019, I will be visiting Deducteam at LSV, Paris/Cachan. There will be two presentations about Isabelle technology for formal documents and libraries:

  1. Interaction with Formal Mathematical Documents in Isabelle/PIDE (with slides) – Tuesday 18-Jun-2019, 11:00, Pavillon du Jardin, ENS Cachan.
  2. Isabelle technology for the Archive of Formal Proofs (with slides) – Thursday 20-Jun-2019, 14:00, LSV library.

See also the official announcement of Deducteam.

Note: These talks will be repeated at the Conference on Intelligent Computer Mathematics (CICM 2019), Prague (CZ), 08..12-Jul-2019.

Interaction with Formal Mathematical Documents in Isabelle/PIDE (at CICM 2019, Prague)

At the Conference for Intelligent Computer Mathematics (CICM 2019) in Prague (08..12-Jul-2019), I will give a keynote presentation on the track Mathematical Knowledge Management (MKM).

Title:
Interaction with Formal Mathematical Documents in Isabelle/PIDE
Abstract:
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized mathematics in Isabelle/HOL. More recently, the scope of PIDE has widened towards languages that are not connected to logic and proof in Isabelle, but taken from a broader repertoire of mathematics on the computer. The present paper provides a general overview of the PIDE project and its underlying document model, with built-in parallel evaluation and asynchronous interaction. There is also some discussion of original aims and approaches, successes and failures, later changes to the plan, and ideas for the future.
Paper:
Preprint from ArXiv

Release Candidates for Isabelle2019

The official Isabelle2019 release is scheduled for mid-June 2019. This blog entry is dynamically updated to follow the sequence of public release candidates.

  • Isabelle2019-RC0 (02-Apr-2019): informal snapshot for experimentation, approx. one month before regular RC1. See also AFP/7c585d0056e3.
  • Isabelle2019-RC1 (03-May-2019): first official release candidate; everything is ready, except for pending updates of documentation (isar-ref and jedit). See also AFP/d50417d0ae64.
  • Isabelle2019-RC2 (11-May-2019): consolidated release candidate and fork-point of isabelle-release vs. isabelle development repositories; see also AFP/2170a6647f04. Notable changes:
    • Update of documentation: isar-ref and jedit.
    • Minor updates of sessions HOL-Analysis and HOL-Data_Structures.
    • Simplified main application bundles: back to .tar.gz for Linux and macOS, auto-installable self-extracting archive for Windows.
    • Elimination of odd Java warnings on macOS.
  • Isabelle2019-RC3 (25-May-2019): refined release candidate, see isabelle-release and afp-2019. Notable changes:
    • Isabelle/jEdit: proper update of Theories panel after Purge operation.
    • Windows: back to default path on desktop (more robust); also applies to auto-installable self-extracting archive.
    • Windows: update to Cygwin 3.0.7.
    • More direct invocation of z3: potentially more robust on Windows.
  • Isabelle2019-RC4 (01-Jun-2019): presumably last release candidate, see isabelle-release and afp-2019. Notable changes:
    • Windows: slightly more robust invocation of z3 and cvc4.
    • Windows: note on website about excluding the Isabelle application directory from Virus & threat protection.
    • macOS: hint about Isabelle/jEdit action isabelle.draft for more robust printing via Web browser.

Update 10-Jun-2019: The final release of Isabelle2019 (June 2019) is available from the Isabelle website. The above release candidates will disappear eventually.

“Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)

The current print edition of Spektrum der Wissenschaft 3.19 includes an article Mathematische Unterhaltungen: Hilbert und Isabelle (by Christoph Pöppe, in German). It recounts the prize-winning project by a group of young students from Bremen, with many explanations about the overall problem and the approach in formalization.

This project is notable as an ambitious proof formalization by genuine end-users of Isabelle, without any previous connections to the providers of the tool. Only after the first public appearance, I have occasionally had a chat with some of the authors, either personally or via email; likewise some of my colleagues.

Isabelle/MMT: export of Isabelle theories and import as OMDoc content

MMT (or “Meta Meta Theory”) is a general framework for formal and informal languages, including lambda-calculus and logic, but also text documents. The documentation provides an overview of the MMT language and system (which is implemented in Scala).

I have collaborated over some months with the makers of MMT: Florian Rabe and Michael Kohlhase. The outcome is Isabelle/MMT, a tool in Isabelle/Scala that uses the MMT library to export Isabelle theory content and import it into MMT as OMDoc files. Robustness and scalability have been of primary concern of Isabelle/MMT: We have managed to process recent Isabelle + AFP within 6.5h on high-end hardware, excluding only very big sessions of AFP (notably the “slow” group).

Here are further technical details:

  • Intel Xeon CPU E5-2699 @ 2.20GHz with 20 cores
  • Poly/ML: 30 GB heap size, approx. 12 active threads
  • Java 11: 30 GB heap size, approx. 2 active threads
  • 540 sessions
  • 5463 theories
  • 1404441 logical items:
    • 4021 locales (including classes)
    • 4057 locale dependencies (sub-locales, sub-classes etc.)
    • 1101 type-classes
    • 9620 types
    • 191336 constants
    • 1194306 theorems
  • 160 MB OMDoc content with XZ compression, or 26 GB uncompressed

The resulting OMDoc content is available from the MathHub service by Kohlhase and Rabe. It is possible to browse it locally via the HTTP server that is included in MMT, e.g. by the command-line wrapper isabelle mmt_server. See also the README (towards the bottom) and the following screenshot:

Isabelle/MMT output via MMT HTTP server

Browsing only works smoothly for small Isabelle theories. The Scala APIs of MMT provide more scalable access to the massive amount of material, e.g. it could be used for “data-mining” of Isabelle/AFP content.

Isabelle export

The Isabelle/MMT export uses new mechanisms from recent repository versions (after the Isabelle2018 release), e.g. see Isabelle_09-Nov-2018. In particular:

  1. Export of “blobs” into the Isabelle session database, e.g. see the export_theory system option and the isabelle dump tool. In such batch-mode tools, exports are written to an SQLite database and dumped to the file-system.
  2. Use of PIDE (Prover IDE) processing under program control: the database content is maintained within the running Java process and later written to OMDoc files. The PIDE session allows to export many details of formally annotated sources: presently only the source positions of declared types, constants, theorems etc. are reconstructed and associated with the corresponding command-span in the text.

Other applications of theory export may be considered, e.g. OpenTheory or Dedukti, but note that proof objects are presently omitted. Full proof terms would require some orders of magnitude more resources. Instead, it is probably better to use structured Isar proof texts with formal PIDE annotations.

MMT import

Import into MMT uses the existing LF library, which provides a Logical Framework that is similar to Isabelle/Pure. Isabelle types, terms, propositions are translated in a straight-forward manner. Type-classes of Isabelle occur here as classes of types, without any additional structure yet. Further theory structure is provided by localesclasses are locales with special link-up with the type-system. Overall we get the following aspects of Isabelle theory content in MMT:

  1. Foundational theory content: type-classes, types, terms (constants), theorems (facts).
  2. Locales (and classes) as “little-theories”: with some information about locale dependencies and locale interpretations.
  3. Limited mixfix/infix syntax for global constants and locale constants.
  4. Original source text for Isabelle/Isar commands that introduce formal content.

More details are possible: Isabelle content is very rich, with many extra-logical aspects. The “flexiformal” approach of MMT might eventually help to express a lot of this, beyond the standard Logical Framework approach.

The Isabelle Prover IDE after 10 years of development

At the Dagstuhl-Seminar 18341 Formalization of Mathematics in Type Theory (19..24-Aug-2018), I delivered a talk on The Isabelle Prover IDE after 10 years of development.

Abstract:

The main ideas around Isabelle/PIDE go back to summer 2008. This is an overview of what has been achieved in the past 10 years, with some prospects for the future. Where can we go from here as Isabelle community? (E.g. towards alternative front-ends like Visual Studio Code; remote prover sessions “in the cloud”; support for collaborative editing of large formal libraries.) Where can we go as greater ITP community (Lean, Coq, HOL family)?

See also the slides.

In the discussion after the talk, there was a very fitting reference to the website of Bret Victor, “perveyor of impossible dreams”.