Visual Studio Code as Prover IDE for Isabelle

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