Category Archives: Isabelle

The Isabelle Prover IDE after 10 years of development

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.

Abstract:

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

Slides for presentations at FLoC 2018 (Oxford)

The slides for my presentations at FLoC 2018 (Oxford) are now available via the official “smart slide” service:

Video for Isabelle/PIDE presentation at Curry Club Augsburg

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.

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.

  • Isabelle2018-RC0 (06-Jun-2018): informal snapshot for experimentation. See also AFP/7f9c8aca53e8.
  • Isabelle2018-RC1 (02-Jul-2018): first official release candidate; almost everything ready, but some documentation still needs update. See also AFP/2af750da996c.
  • Isabelle2018-RC2 (22-Jul-2018): consolidated release candidate (after attending FLoC 2018 at Oxford). See also AFP/7175b64d54a4. Notable changes:
    • Update of Poly/ML component: slightly improved performance and more robust.
    • Update of Kodkodi component for Nitpick on Windows (back to status-quo from Isabelle2017).
    • Session HOL-Real_Asymp by Manuel Eberl.
    • Further library tuning of HOL, HOL-Analysis, HOL-Algebra.
  • Isabelle2018-RC3 (29-Jul-2018): fairly stable release candidate. See also AFP for Isabelle2018. Notable changes:
    • Update of Poly/ML component: proper monitoring of ML threads.
    • Update to latest Java 8 release: jdk-8u181.
    • More command-line options for isabelle vscode_server (relevant for VSCode settings isabelle.args).
    • Isabelle Server: allow to specify timeout for use_theories.
    • Proper treatment of forked proof within context of subgoal premises.
    • More robust build of HOL-Proofs with threads=2.
    • More flexible document build script.
    • Clarified word characters in Isabelle/jEdit to accommodate \<^control> symbols.
  • Isabelle2018-RC4 (07-Aug-2018): presumably the last release candidate. See also AFP for Isabelle2018. Notable changes:
    • Update of Isabelle/jEdit manual.
    • Fine-tuning of isabelle build options -c -x -B.
    • Fine-tuning of Isar command span range: relevant for checking of formal comments.
    • Removed Sledgehammer prover veriT: not ready for release.

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.

Update 15-Aug-2018: The final release of Isabelle2018 (August 2018) is available from the Isabelle website. The above release candidates will disappear eventually.

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 www.DeepL.com/Translator)

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.

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.

The Isabelle Server: responsive control of prover sessions

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.