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

Flattr this!

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.

Flattr this!