Overview of Bu's commented Isabelle
Personnes présentes
- Du Zeye
- Burkhart Wolff
- Frédéric Boulanger
- Chantal Keller
- Safouan Taha
- Benoît Valiron
Presentators (by order of appearance)
- Burkhart Wolff
Content
The objective is to get something close to
The Isabelle Cookbook,
but have it automatically checkable, so that one can automatically track API changes along different version changes of Isabelle.
In this seminar, Bu goes over Isabelle Nano-Kernel and LCF kernel using annoted Isabelle signatures and ML code. The presentation is based on an .thy document
My Commented Isabelle
which is structured itself following a TechReport-ontology supported in the
Isabelle Document Ontology Framework (DOF)
containing facilities for having Isabelle comments automatically typed and proof-checked by the kernel, in a Smalltalk-like way. DOF helps here in tracing the dependencies and helping to generate the TR-.pdf at a snip without touching LaTeX (or nearly).
0 - Preliminaries
The main Isabelle theory is found in the repository for Isabelle/DOF :
A PDF file is automatically built from the theory, and can serve as an official offline reference.
However, the main interest of this theory is when used within Isabelle: one can then rely on the interactive links to browse both the file and the Isabelle architecture.
To use it within Isabelle:
- Install Isabelle/DOF: https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/
- Within Jedit, load the file src/branch/master/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy
- Load ROOT.ML
- The interactive links allow the user to browse the code.
2 - Prover Architecture
This section summarizes the content of the file, as described by Bu during his presentation.
2.1 - The Nano-kernel
Isabelle stack:
- Foundations: SML System, Boot-Order, System Architecture
- Prover-achitecture: N1-Kernel LCF-Kernel
- Front-End architecture: parsers, markup, PIDE, and stuff
- System Issues: Code Generation, Build Management
Bu goes through the the Isabelle stack and the bootstraping phases as seen in the source code:
Abstract Isabelle Architecture
In practice, though, are cycles in the system architecture (for system parsers and pretty-printers) resolved with hooks. (see for the PDF file for details).
There are actually two SML interpreters (or one with 2 different environments ("toplevels"))
- the "real one" fired when running the command polyml, for example, and
- the one you get inside Isabelle when issuing "ML < stg >" called Isabelle/ML
- Isabelle/ML allows you to have acces to code-antiquotations; this anti-quotation language is extensible,
- the namespaces are different, and
- there are bridges but ideally you cannot "break" Isabelle through this top-level.
The Nano-Kernel was originally written by Makarius.
There, a context is a container with an id, a list of parents (i.e. a graph), a timestamp, and a sub-context relation.
Isabelle is different from other HOL's : if want to transport a proof in another theory -- a super-context, then there is an explicit rule for it in the language. Unlike HOL4 where the proof is reconstructed in the new context.
Context comes in various flavors:
- Theories
- Proof-Contexts
- Generic, i.e. sum of both.
2.2 - The LCF-kernel
Based on these, one can build something closer to what we would call logical kernel.
It consists of a small lambda-calculus with de Brujin indices. There is a "dummy" term "dummyT".
One can check that a type annotation is consistent with the module "Sign"
The type inference algorithm gets rid of "joker"-like things such as "dummyT", which is translated to fresh schematic type variables, which were instantiated by some variant of Milners W algorithm.
A detailed interactive example can be found in My Commented Isabelle, this is helpful since the interfaces are at times quite obscured by non-conform type-synonyms and lack of documentation at this level.
3 - Front-End
Presented in the next episode!