On Thu 14-Jun-2018 I will talk about Isabelle/jEdit as Formal IDE at Curry Club Augsburg.
Start: approximately 19:00.
Duration: undefined.
Language of the talk: German
Slides: PDF
This is a spin-off from the paper that I will present at the F-IDE workshop on Sat 14-Jul-2018 in Oxford.
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.
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:
isabelle server &
isabelle client
session_start {"session": "HOL"}
use_theories {"session_id": ..., "theories": ["~~/src/HOL/ex/Seq"]}
session_stop {"session_id": ...}
shutdown
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.
Update 12-Jul-2018: Link to forthcoming Isabelle2018.
Isabelle applications (e.g. from AFP) are growing steadily in size and number. To outline requirements and possibilities of the technology, I have produced a document on Scaling Isabelle Proof Document Processing.
Abstract:
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).
On 23-Nov-2017, I will give a presentation about Future Prospects of Isabelle Technology at DTU (Danmarks Tekniske Universitet), Copenhagen – thanks to an invitation by Jørgen Villadsen. More information on the meeting is available on the website.
Abstract:
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.
Sources for the presentation: Copenhagen2017.tar.gz
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).
On Mon 24-Jul-2017, I gave a presentation at the BigProof event in Cambridge. Title: The Isabelle Prover IDE (PIDE) after 9 years of development, and beyond. Abstract:
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:
Microsoft is more and more becoming an Open Source company, e.g. it has joined the Linux foundation as Platinum member in November 2016. A notable Open Source project by Microsoft is Visual Studio Code: under the slogans “Code editing. Redefined. Free. Open Source. Runs everywhere.” it provides a very interesting editor framework, as a desktop application based on Node.js and TypeScript.
The prover community has already started to support this emerging successor of vi and Emacs, e.g. see Coq Support for Visual Studio Code and the Lean for VSCode.
Isabelle/VSCode is now following this trend: I have spent some weeks in December 2016 / January 2017 with VSCode, using a little bit of TypeScript and implementing the new Language Server Protocol in Isabelle/Scala. The subsequent screenshot shows formal annotations produced by Isabelle/PIDE in the usual manner, while the editor rendering is all done by VSCode. For more information, see the report Isabelle/VSCode in January 2017.
The Isabelle/VSCode project was funded by Aesthetic Integration (AI). See also my article about a talk at ITP 2016 by Grant Passmore (co-founder of AI).
On Friday 18-Nov-2016 10:00, I will give a presentation about PIDE at Laboratoire de Recherche en Informatique, Orsay (Paris Sud).
Abstract:
Isabelle is usually positioned as environment for interactive and automated theorem proving, but its Prover IDE (PIDE) may be used for regular program development as well. Standard ML is particularly important here, since it is the bootstrap language of Isabelle/ML (i.e. SML with many add-ons) and Isabelle/Pure (i.e. the logical framework).
The ML IDE functionality of Isabelle + Poly/ML is manifold:
- Continuous feedback from static analysis and semantic evaluation is already available for years, e.g. Isabelle2014 (August 2014). It is a corollary of how PIDE interaction works, and of the integration of the Poly/ML compiler into that framework. Source files are statically checked and semantically evaluated while the user is editing. The annotated sources contain markup about inferred types, references to defining positions of items etc.
- Source-level debugging within the IDE is new in Poly/ML 5.6, which is bundled with Isabelle2016 (February 2016). The Prover IDE provides the Debugger dockable to connect to running ML threads, inspect the stack frame with local ML bindings, and evaluate ML expressions in a particular run-time context. See also here.
- IDE support for the Isabelle/Pure bootstrap process is new technology for the coming release of Isabelle2016-1 (December 2016). The ROOT.ML file acts like a quasi-theory in the context of theory ML_Bootstrap: this allows continuous checking of all loaded ML files. The theory file is presented with a modified header to import Pure from the running Isabelle instance.
It is also possible to modify standalone SML projects, to edit the sources freely in the ML IDE. For example, MetiTarski can participate after some trivial changes of its ROOT.ML file.
Overall, we move more and more to an integrated framework for development of formal-reasoning tools, but other applications are admissible as well.
The Slides are available, together with their sources (which are required for the live system demo).
On Tuesday 15-Nov-2016 14:00, I will give a presentation about PIDE at Laboratoire Spécification et Vérification, Cachan (Paris). See also the official announcement.
Abstract:
Interactive theorem proving was historically tied to the read-eval-print loop, with sequential and synchronous evaluation of prover commands given on the command-line. This user-interface technology was adequate when Robin Milner introduced his LCF proof assistant in the 1970s, but today it severely restricts the potential of multicore hardware and advanced IDE front-ends.
The Isabelle Prover IDE breaks this loop and retrofits the read-eval-print phases into an asynchronous model of document-oriented proof processing. Instead of feeding a sequence of commands into the prover process, the primary interface works via edits over immutable document versions. Execution is implicit and managed by the prover in a timeless and stateless manner, making adequate use of parallel hardware.
PIDE document content consists of the theory sources (with dependencies via theory imports), and auxiliary source files of arbitrary user-defined format: this allows to integrate other languages than Isabelle/Isar into the IDE. A notable application is the Isabelle/ML IDE, which can be also applied to the system itself, to support interactive bootstrapping of the Isabelle/Pure implementation.
Further tool integration works via “asynchronous print functions” that operate on already checked theory sources. Thus long-running or potentially non-terminating processes may provide spontaneous feedback while the user is editing. Applications range from traditional proof state output (which often consumes substantial run-time) to automated provers and dis-provers that report on existing proof document content (e.g. Sledgehammer, Nitpick, Quickcheck in Isabelle/HOL). It is also possible to integrate “query operations” via additional GUI panels with separate input and output (e.g. for manual Sledgehammer invocation or find-theorems).
Thus the Prover IDE orchestrates a suite of tools that help the user to write proofs. In particular, the classic distinction of ATP and ITP is overcome in this emerging paradigm of Integrated Theorem Proving.
The Slides are available.