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
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 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.
We are heading towards the Isabelle2017 release, which is scheduled for October 2017. This spot provides a reference for upcoming release candidates.
As usual, 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, not after it.
The main forum for discussion of Isabelle2017 release candidates is on isabelle-users mailing list.
Update 09-Oct-2017: The final release of Isabelle2017 (October 2017) is now available from the Isabelle website. The above release candidates will disappear eventually.
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:
Here is an interesting (draft) paper about Social Network structures in the Isabelle and Coq community, based on the main mailing lists of the two systems:
J. Fleuriot, S. Obua, Ph. Scott: Social Network Processes in the Isabelle and Coq Theorem Proving Communities. arXiv:1609.07127, September 2016.
Just a few comments of mine:
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).
Another Isabelle presentation at Curry Club Augsburg (01-Dec-2016) has been recorded and uploaded to Youtube.
See also the original announcement.
On Thu 01-Dec-2016 there will be a presentation about “Foundations of Higher-Order Logic with Classical Reasoning and Hilbert-Choice” at Curry Club Augsburg.
Start: approximately 19:00
Duration: approximately 90min
Language of the talk: German
- History of Higher-Order Logic
- Implementations of HOL
- Quasi-programming in Isabelle/HOL
- Isabelle foundations: primitive inferences, object-logic rules, rule composition, structured proofs
- Foundations of Higher-Order Logic: actual Isabelle/HOL, Pure bootstrap of HOL
Isabelle theory with some exercises (for Isabelle2016-1)
The coming Isabelle2016-1 release is scheduled for December 2016. This spot is continuously updated to inform about the ongoing process of testing release candidates.
- On 07-Oct-2016 an informal snapshot Isabelle2016-1-RC0 was published.
- On 28-Oct-2016 the release candidate Isabelle2016-1-RC1 was published. Serious testing by users is now required, to expose remaining problems.
- On 06-Nov-2016 the release candidate Isabelle2016-1-RC2 was published. Various details have been consolidated.
- On 22-Nov-2016 the release candidate Isabelle2016-1-RC3 was published. More fine points have been consolidated. A component for the new experimental Nunchaku tool has been included.
- On 27-Nov-2016 the release candidate Isabelle2016-1-RC4 was published. It introduces the following important last-minute changes:
- Prover IDE: more aggressive flushing of machine-generated input
- Sledgehammer: MaSh is faster and less likely to hang seemingly forever
- fine-tuning of Isabelle/LaTeX typesetting
- On 08-Dec-2016 the release candidate Isabelle2016-1-RC5 was published, presumably the last one. It introduces the following important last-minute changes:
- more uniform automatic indentation (empty vs. non-empty lines)
- fewer tracing/warning messages in some proof tools
The Isabelle release process is subject to the laws of causality: release candidates can be modified, but the final release remains final. Testing needs to happen in the weeks before the final release, not after it.
The main forum for discussion of Isabelle2016-1 release candidates is on isabelle-users mailing list.
Update 13-Dec-2016: The final release of Isabelle2016-1 (December 2016) is now available from the Isabelle website. The above release candidates will disappear eventually.