Monthly Archives: January 2017

Isabelle, PIDE

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

Admin

Provider change for sketis.net

After almost 12 years I have now changed the provider for sketis.net. This is the first post on the new platform, as a constructive proof that it really works!

Moving a classic toplevel domain (like .net) requires extra care and extra time. For almost 2 weeks nothing happened. Then there was a mail indicating failure of the procedure. After restarting the process it worked out surprisingly fast, within only 1 day instead of 5 days specified in the official mail text.

Now it might require additional 48h until the last corner of the Internet has noticed the new address of http://sketis.net.