Yamma's a Metamath proof assistant for Visual Studio Code.
A language server for .mmp files (metamath proof files).
- Completions: syntax suggestions, step suggestions, search results
- Diagnostics
- Code Actions
- Quick Fixes: missing disjoint vars statements
- Semantic Tokenization
- On Hover Documentation
- Unification: standard reformatting, renumbering, step completion, step derivation
- Search in the theory
- Step Suggestions (Model Based)
- Model Generation
- Proof Generation
- Load/Save additional theorems in .mm compatible format
To use this extension, you need to have Node.js installed on your machine. If Node.js is not yet installed, follow the official installation guide: Node.js Installation Guide.
- Launch Visual Studio Code.
- Go to the Extensions view by clicking on the square icon on the left sidebar or pressing
Ctrl+Shift+X. - Search for "Yamma" in the search bar.
- Click on the "Install" button next to the "Yamma" extension.
- After the installation, click on the "Reload" button to activate the extension.
- Open a .mmp file in Visual Studio Code
- If a file set.mm is found in the same folder, the extension will automatically use it as the underlying theory: it will be loaded, parsed, and verified
- If no .mm file is automatically found, click on the Gear icon next to the extension's name and select Extension Settings from the dropdown menu. This action opens the settings for Yamma: here you can insert the exact path to the .mm file to be used
- Use the command palette (
Ctrl+Shift+PorCmd+Shift+Pon macOS) to access the available commands and features provided by the extension - Utilize the Intellisense capabilities to get suggestions while writing your proofs
- Once your proof is complete, you can use the "Unify and store in MMT folder" contextual menu command to generate an MMT file, ready to be copied and pasted into your main MM file.
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