Category Archives: Isabelle

Isabelle/jEdit as Formal IDE at Curry Club Augsburg

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.

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.

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.

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

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.


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?

The Isabelle Server: responsive control of prover sessions

Recent Isabelle repository versions (e.g. 83902fff6243) 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": ...}

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.

Further Scaling of Isabelle Technology

On Monday 05-Feb-2018, I will give a presentation about Further Scaling of Isabelle Technology at VU Amsterdam, invited by Jasmin Christian Blanchette. See also the official seminar website.


Over 32 years, Isabelle has made a long way from a small experimental proof assistant to a versatile platform for proof document development and maintenance. There has always been a challenge to keep up with the natural growth of applications, notably the Archive of Formal Proofs (AFP).

  • Can we scale this technology further, towards really big libraries of formalized mathematics?
  • Can the underlying Scala/JVM and Poly/ML platforms cope with the demands?
  • Can we eventually do 10 times more and better?

I will revisit these questions from the perspectives of

  1. Editing: Prover IDE,
  2. Building: batch-mode tools and background services,
  3. Browsing: HTML views and client-server applications.

Scaling Isabelle Proof Document Processing

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.


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

Future Prospects of Isabelle Technology

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.


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

Isabelle/VSCode 1.0 in Isabelle2017

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

Isabelle Docker image

The new Isabelle2017 distribution provides a Docker image via the Docker Hub repository.

The Docker image contains Ubuntu Linux with Isabelle2017. It can be used, e.g. on another Linux host like this:

  • docker pull makarius/isabelle:Isabelle2017
  • docker run makarius/isabelle:Isabelle2017

That provides command-line access to the regular isabelle tool wrapper, with indirection through the Docker container infrastructure.

The image already contains ML heaps for Isabelle/Pure and Isabelle/HOL. Here is an example to build more:

  • docker run makarius/isabelle:Isabelle2017 -s -b HOL-Library

Note that Docker is mainly for command-line tools on the “Cloud”. There is presently no Isabelle Prover IDE support, although very old-fashioned X11 connections can be made to work with extra tinkering.