nanoCRL2 LSP

A language server protocol (LSP) implementation of the mCRL2 model checking language.

Current version: 0.3.0

Features

The following features are currently planned, where the fully implemented features are crossed off:

• [x] Static syntax highlighting of .mcrl2 files
• [x] Parsing error detection
• [x] Symbol renaming
• [x] Basic language configuration stuff (matching braces, comment styles, etc.)
• [x] Auto-complete
  • [x] With snippets that show parameters
• [x] Go to definition
• [x] Show references
• [x] Syntax errors (on save)
• [ ] Semantic syntax highlighting of .mcrl2 files
• [ ] Custom commands to run mCRL2 tools with Ctrl+Shift+P
• [ ] Static syntax highlighting of .mcf files
• [ ] Semantic syntax highlighting
• [ ] Project file integration, reading of .mcrl2proj files, and understanding referencing of .mcrl2 files from .mcf files
• [ ] Documentation when hovering over symbols

The following platforms are supported:

• [x] Windows
• [x] MacOS
  • [x] aarch64 AKA arm64 AKA Apple Silicon
  • [x] x64
• [x] Linux

Licensing

The client implementation and other JavaScript boilerplatse in this repository is based on the tower-lsp boilerplate repository. The license for that can be found in ./LICENSE.

The code in the ./server directory is my own and is separate from the client implementation. As such, I own its copyright and it has its own license.

Technical Details

The extension implements the LSP, meaning it should be easy to add support for other clients. Right now it only supports VSCode/VSCodium however.

I use my own nanoCRL2 library for this extension instead of the original mCRL2 implementation. This is because that implementation is not really made to be used by a language server. On the other hand, nanoCRL2 is a more lightweight, query-based compiler with no global state, which has the advantage that editor features can call arbitrary semantic analysis passes and only pay for the parts that are strictly necessary. For instance, if you want to ctrl-click on a symbol to "go to definition", the compiler only runs the name lookup pass for that symbol (i.e., it does not run the entire compiler pipeline to find the location of the definition of one symbol).

Building and Running Locally

Run npm i and then npm run build in the root directory. Also run cargo build in the server/ directory. You can then press F5 in VSCode to test this extension locally.

Publishing

Run npm i and then bundle appropriately by using npm run build (which uses esbuild).

Run cargo build --release and copy the nano-crl2-lsp executable into the server/ folder, and rename it to nano-crl2-lsp-linux.

Run cargo build --release --target x86_64-pc-windows-gnu, copy the nano-crl2-lsp.exe executable there, and rename it to nano-crl2-lsp-win32.exe. (Or if you are on windows, you have to cross-compile the other way around.)

Also compile two versions on a Mac computer (or somehow cross-compile if you have the skill to figure this out): one with --target aarch64-apple-darwin, renamed to nano-crl2-lsp-aarch64-apple-darwin, and one with --target x86_64-apple-darwin, renamed to nano-crl2-lsp-x86_64-apple-darwin.

Finally, delete the server/target/ directory, because it takes up a lot of space.

For publishing the VSCode extension, refer to Publishing Extensions.

For publishing the VSCodium extension, refer to Publishing Extensions. I publish to namespace nano-crl. I run ovsx publish -p <token> (optionally with flag --pre-release), which should also run npm run build automatically.