nano-crl2-lsp

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

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
• [ ] Go to definition (partially done, does not work well with overloaded definitions)
• [ ] Show references (same situation)
• [ ] 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
• [ ] MacOS
• [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). Also, run cargo build --release and copy the nano_crl2_lsp executable into the server/ folder, and run cargo build --release --target x86_64-pc-windows-gnu and copy the nano_crl2_lsp.exe executable there too. (Or if you are on windows, you have to cross-compile the other way around.) 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.