Isabelle/VSCode: Editor Improvements and Prover IDE integrations

Chair for Logic and Verification

Bachelor Thesis

With the emergence of the language server protocol (LSP) [1], integrating new languages and frameworks into existing modern IDEs has become a feasible task. For the interactive theorem prover Isabelle, a Visual Studio code (VScode) plugin has already been introduced [2], which is makes it possible to develop formal theories in a more common IDE than the highly adapted Isabelle/jEdit.

However, Issues with mathematical symbols, slow highlighting for large theory files, partially missing markup make this plugin difficult to use. Moreover, many semantic IDE features are absent.

The task of this thesis is to rework the Isabelle/VScode integration in order to provide first-level support of Isabelle symbols and markup, as well as adding support for important Prover IDE functionality. While the backend Isabelle functionality is built in Scala, the frontend functionality of VSCode is based on web technologies.

Your implementation will also be valuable for further developments of Isabelle/jEdit, since future plans involve migrating that frontend to a web-based stack as well.

Prerequisites

Typescript/Web Development Experience; Scala (or similar functional programming language); English

Advisor

Fabian Huch, email {huch} AT [in.tum.de]

Supervisor

Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]

References

[1] Language Server Protocol

[2] Wenzel, Makarius. “Isabelle/PIDE after 10 years of development.” UITP workshop: User Interfaces for Theorem Provers. 2018.

Results

First thesis in PDF format

Second Thesis in PDF format

Students

Denis Paluca Thomas Lindae