Category Archives: Isabelle

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”.

Slides for presentations at FLoC 2018 (Oxford)

The slides for my presentations at FLoC 2018 (Oxford) are now available via the official “smart slide” service:

Video for Isabelle/PIDE presentation at Curry Club Augsburg

Here is the video for the Isabelle/PIDE presentation at Curry Club Augsburg from 14-Jun-2018:

There are some technical challenges: missing screen recording in the first 25min, and occasional changes in the speed of screen recording later on: sometimes the computer screen is ahead of the talk. Nonetheless, this is an opportunity to learn many things about Isabelle/PIDE, how it is done, why it is done like that.

Release candidates for Isabelle2018

We are heading towards the Isabelle2018 release, which is scheduled for August 2018. This spot provides a reference for upcoming release candidates.

  • Isabelle2018-RC0 (06-Jun-2018): informal snapshot for experimentation. See also AFP/7f9c8aca53e8.
  • Isabelle2018-RC1 (02-Jul-2018): first official release candidate; almost everything ready, but some documentation still needs update. See also AFP/2af750da996c.
  • Isabelle2018-RC2 (22-Jul-2018): consolidated release candidate (after attending FLoC 2018 at Oxford). See also AFP/7175b64d54a4. Notable changes:
    • Update of Poly/ML component: slightly improved performance and more robust.
    • Update of Kodkodi component for Nitpick on Windows (back to status-quo from Isabelle2017).
    • Session HOL-Real_Asymp by Manuel Eberl.
    • Further library tuning of HOL, HOL-Analysis, HOL-Algebra.
  • Isabelle2018-RC3 (29-Jul-2018): fairly stable release candidate. See also AFP for Isabelle2018. Notable changes:
    • Update of Poly/ML component: proper monitoring of ML threads.
    • Update to latest Java 8 release: jdk-8u181.
    • More command-line options for isabelle vscode_server (relevant for VSCode settings isabelle.args).
    • Isabelle Server: allow to specify timeout for use_theories.
    • Proper treatment of forked proof within context of subgoal premises.
    • More robust build of HOL-Proofs with threads=2.
    • More flexible document build script.
    • Clarified word characters in Isabelle/jEdit to accommodate \<^control> symbols.
  • Isabelle2018-RC4 (07-Aug-2018): presumably the last release candidate. See also AFP for Isabelle2018. Notable changes:
    • Update of Isabelle/jEdit manual.
    • Fine-tuning of isabelle build options -c -x -B.
    • Fine-tuning of Isar command span range: relevant for checking of formal comments.
    • Removed Sledgehammer prover veriT: not ready for release.

The Isabelle release process is subject to the laws of causality: release candidates can be modified, but the final release is unchangeable. This means that testing needs to happen in the weeks before the final release.

The main forum for discussion of Isabelle2018 release candidates is on isabelle-users mailing list.

Update 15-Aug-2018: The final release of Isabelle2018 (August 2018) is available from the Isabelle website. The above release candidates will disappear eventually.

Jugend forscht: Hilbert meets Isabelle

A group of smart students from Bremen have been working on a formalization of Hilbert’s 10th Problem (DPRM Theorem) in Isabelle since October 2017. See also the forthcoming presentation on the Isabelle Workshop 2018 (13-Jul-2018, Oxford, UK) with the following pre-print paper.

A subgroup of particularly young students have also submitted their contribution to the project in the German science competition “Jugend forscht”, and have now won various prizes, notably the “Prize for Extraordinary Work” by Federal President of Germany, Frank-Walter Steinmeier. The catalog of winners lists the project on page 4, with the following laudatio:

Die Jury war begeistert von der Tiefe und begrifflichen Präzision, mit der sich die drei Jungforscher dem komplexen Thema des formalen Verifizierens annahmen. Formale Verifikation ist ein hochaktuelles und wichtiges Thema. Die anspruchsvolle und außergewöhnliche Forschungsarbeit leistet einen wichtigen Beitrag, die Fundamente der Mathematik noch ein Stück stabiler zu machen.

The jury was enthusiastic about the depth and conceptual precision with which the three young researchers addressed the complex topic of formal verification. Formal verification is a highly topical and important topic. The demanding and extraordinary research work makes an important contribution to making the foundations of mathematics even more stable.
(Translated with www.DeepL.com/Translator)

There are some sources and presentation materials on GitLab.

The Isabelle community is looking forward to the final completion of the formalization!

Isabelle/jEdit as formal IDE

This is my contribution to the F-IDE workshop (14-Jul-2018, Oxford, UK): Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents.

Abstract:

Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?

See also the official slides.