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:Isabelle2017docker 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.
Website of Dr. Makarius Wenzel