Yamma's a Metamath proof assistant for Visual Studio Code.
A language server for .mmp files (metamath proof files).
This Language Server works for .mmp files. It has the following language features:
- Code Actions
- Quick Fixes
- Semantic Tokenization
- On Hover Documentation
- Unification (and Standard Reformatting)
- Search (in the theory)
- Step Suggestions (Model Based)
- Model Generation
- Load/Save additional theorems in .mm compatible format
First please ensure you have git, nodejs, and Visual Studio Code installed. Then:
git clone https://github.com/glacode/yamma.git
The final command opens Visual Studio Code, within it we can:
- From the side-bar on the far left, choose "Run and Debug".
- Open the Run and Debug drop-down.
- Choose "Launch Client" from the drop-down.
- Press the play icon ("Start Debugging").
This runs a second instance of Visual Studio Code. This instance is running the Yamma extension. The first time in here we will want to open the settings and set a path to a valid .mm file.
- From the side-bar on the far left, choose "Manage".
- From the menu this brings up, choose "Settings".
- From the bottom of the list of settings, expand "Extensions".
- From the list of extensions, click on "Yamma"
- In the "Mm File Full Path" box, enter the full path to a valid .mm file.
Now when we have a .mmp file open in this instance of Visual Studio Code, Yamma provides the following keyboard commands (on a Mac we may need to use the command key rather than the CTRL key):
- CTRL+U Unify
- CTRL+H Search