At the Dagstuhl-Seminar 18341Formalization 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)?
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.
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?
Recent Isabelle repository versions (e.g. 83902fff6243 as approximation of Isabelle2018) support client-server connections for Isabelle prover sessions, with a
simple line-based protocol for synchronous commands. Asynchronous tasks work by explicit indication of forked vs. finished (or failed) background processes, potentially with intermediate notifications. Protocol messages use JSON syntax by default, but YXML is also possible (e.g. for native PIDE messages that might be supported in the future).
Further details are explained in chapter 4 of the system manual, e.g. see the Documentation panel in Isabelle/jEdit of a recent release snapshot. Here is a minimal example extracted from the manual:
The first two commands are for the Unix terminal, the rest for the Isabelle client-server loop. Each line needs to be applied carefully, when the previous command has finished, and use_theories needs to fit on a single line.
Under program control, explicit messages for forked and finished tasks (with unique id) may be used to enforce execution in the proper order.
This is a study of performance requirements, technological side-conditions, and possibilities for scaling of formal proof document processing in Isabelle and The Archive of Formal Proofs (AFP). The approaches range from simple changes of system parameters and basic system programming with standard APIs to more ambitious reforms of Isabelle and the underlying Poly/ML system. The running examples for typical scalability issues are existing formalizations of classical analysis and differential equations. Such applications can be further extrapolated towards a development of Financial Mathematics (e.g. Itô calculus).
In the past 3 decades, Isabelle has made a long way from a modest LCF-style proof assistant (with copy-paste of proof scripts written in ML) to the current Isabelle/PIDE editor-environment (with its timeless and stateless processing of proof documents). In this presentation, I will try to extrapolate this into the future: How far can we scale proof documents and libraries, e.g. via moving Isabelle into the “cloud”? How can we reduce system resource requirements on the client side? How can we upgrade interactive edits produced by a single author, towards versioned changesets by multiple or distributed authors? What are suitable frameworks for the next generation of Isabelle document preparation? What can we make out of Isabelle/ML as ultra-clean environment for functional programming? Etc. etc.
The new Isabelle2017 release includes support for VSCode as alternative Prover IDE front-end. This continues earlier experiments and is released as Isabelle/VSCode 1.0. Note that Isabelle/jEdit had its 1.0 release in October 2011 and is presently at version 9.0.
Isabelle2017 provides the main Isabelle/Scala/PIDE functionality to connect to VSCode, using the official Language Server Protocol (with some PIDE add-ons). The front-end requires the extension called “Isabelle2017” from the VSCode marketplace: its README provides more information and installation instructions.
The Isabelle/VSCode project has been made possible thanks to funding by Aesthetic Integration (Grant Passmore and Denis Ignatovich).
The main ideas around Isabelle/PIDE go back to summer 2008. This is an overview of what has been achieved in the past 9 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)?
Here are some notable VSCode projects that were briefly mentioned in the talk: