The official Isabelle2019 release is scheduled for mid-June 2019. This blog entry is dynamically updated to follow the sequence of public release candidates.
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.
Gnucash ist ein alt-ehrwürdiges Open-Source Produkt zur Verwaltung von Konten, mit reichhaltigen Möglichkeiten zur Erstellung von “Reports”. Dazu verwendet man in erster Linie den Scheme-Dialekt “Guile”.
Hier das Ergebnis einer Programmierübung in Gnucash / Guile, zum Export von Konten im aktuellen CSV Format der DATEV. Das README enthält eine Reihe nützlicher Referenzen auf Beschreibungen des Formats und frühere Implementierungen.
Achtung: Dies ist im Moment nur für einfache Buchführung zu gebrauchen. Das Gegenkonto (die “Kontra-Rolle”) ist hier stets 1486 nach dem deutschen Standardkontenrahmen 04 (SKR04).
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:
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.
The Isabelle/MMT export uses new mechanisms from recent repository versions (after the Isabelle2018 release), e.g. see Isabelle_09-Nov-2018. In particular:
- Export of “blobs” into the Isabelle session database, e.g. see the
export_theorysystem option and the
isabelle dumptool. In such batch-mode tools, exports are written to an SQLite database and dumped to the file-system.
- 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.
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 locales — classes are locales with special link-up with the type-system. Overall we get the following aspects of Isabelle theory content in MMT:
- Foundational theory content: type-classes, types, terms (constants), theorems (facts).
- Locales (and classes) as “little-theories”: with some information about locale dependencies and locale interpretations.
- Limited mixfix/infix syntax for global constants and locale constants.
- 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 kernel update
linux-image-4.15.0-36-generic (Oct-2018) introduces a timing problem with socket communication in the Isabelle Prover IDE, notably Isabelle/jEdit. Thus loading big sessions becomes very slow (e.g. theory
This can be avoided by downgrading to
linux-image-4.15.0-34-generic or by using the following temporary workaround for Isabelle2018.
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.
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”.
The slides for my presentations at FLoC 2018 (Oxford) are now available via the official “smart slide” service:
- Further Scaling of Isabelle Technology (with paper), on Fri 13-Jul-2018 at the Isabelle workshop
- Isabelle/PIDE after 10 years of development (with paper), on Fri 13-Jul-2018 at the UITP workshop
- Isabelle/jEdit as IDE for domain-specific formal
languages and informal text documents (with paper via EPTCS), on Sat 14-Jul-2018 at the F-IDE workshop
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.