Isabelle/VSCode Prover IDE

General notes

This is the Isabelle/VSCode extension to connect VSCodium to Isabelle/PIDE. The application is invoked via isabelle vscode on the command-line. It takes care about configuring the extension and user settings.

The implementation is centered around the VSCode Language Server Protocol (LSP), but there are many add-ons that are specific to Isabelle/PIDE. Moreover, there are important patches to the VSCodium code-base itself, e.g. to support the UTF-8-Isabelle encoding for mathematical symbols and to incorporate the corresponding Isabelle fonts. It is unlikely that this extension will with regular VSCode nor with any other LSP-based editor.

Isabelle/VSCode works best when opening an Isabelle project directory as a "workspace", with explorer access to the sources. Afterwards it is possible to edit .thy and .ML files with semantic checking by the prover in the background, similar to Isabelle/jEdit. There is also support for other file formats, e.g. bib for bibliographic databases, which may be combined with a regular VSCode extension for LaTeX/BibTeX.

Known limitations of Isabelle/VSCode

• Lack of formal editor perspective in VSCode: only the cursor position is used (with some surrounding lines of text).

• Lack of pretty-printing (logical line breaks) according to window and font dimensions.

• Big theory files may cause problems to the VSCode rendering engine, since messages and text decorations are applied to the text as a whole (cf. the minimap view).

• Overall lack of features and refinements compared to Isabelle/jEdit.

Compile Steps

npm install
npm run compile
npm install -g @vscode/vsce
vsce package