A Visual Studio extension and LSP server for Metamath

The server is still in an early experimental state. It is usable but many advanced features have not yet been implemented.

Install Visual Studio Code, and install rust if not already on your system. Then, install the Metamath LSP server. Until metamath-knife and metamath-vspa are delivered as crate.io crates, this has to be done manually:

git clone https://github.com/tirix/metamath-vspa.git
cargo install --path metamath-vspa/metamath-lsp

This shall compile and install the LSP server mm-lsp-server binary, accessible from your default path.

You can then install the Visual Studio Code extension. There are several possible ways for that:

• in a web browser, from the extension's Visual Studio Code Marketplace web page, press the green "install" button,
• in Visual Studio Code, from the View/Extensions menu, search for Metamath "A Metamath proof assistant" (tirix.metamath), and press the blue "install" button.
• in Visual Studio Code, use Quick Open (Ctrl-P on Windows/Linux, Cmd-P on MacOS), paste ext install tirix.metamath in the box and hit Enter (Return).

See also the extension instructions for how to configure the extension and as a Metamath workspace.

It also possible to launch the extension from the source, using Visual Studio Code itself, for example if you wisth to modify it and contribute to the project:

• Open the directory metamath-vspa/metamath-vscode
• Install node.js and npm
• Launch npm install to install pre-requisites
• Choose 'Run/Start Debugging' from the menu or hit the corresponding shortcut (F5)

• Hovering over a label provides the statement information (hypotheses, assertion, associated comment),
• The "Go to definition" command, when performed on a label, leads to the corresponding statement's definition,
• The "Show Proof" context menu opens a theorem's proof in a new editor tab,
• Diagnostics for the opened Metamath data

Preview:

• Hover and go to definition:

• Outline, problems and show proof:

• Unification, first version:

• This server is based on Mario Carneiro's LSP server for MM0.
• Its core functions are provided by the metamath-knife library, initially by Stefan O'Rear.
• Metamath syntax highlighting is based on Li Xuanji's work in his vscode extension.