Supporting Rzk in VSCode (rzk-1-experimental-highlighting)
Syntax and semantic highlighting for rzk, an experimental proof assistant for synthetic ∞-categories, as well as automatic typechecking.
Features:
- Basic syntax highlighting with a simple TextMate grammar (for
*.rzk, *.rzk.md, and *.rzk.tex files).
- Semantic highlighting via LSP (you must have
rzk version v0.11.0 or above).
- Prompts for installing/updating
rzk binaries from GitHub Releases automatically (usable from local Terminal). Set rzk.manageInstallation to "always" to let the extension install and update rzk for you even when rzk is already available in PATH.
- Markdown Preview button for
*.rzk.md files.
- Automatic typechecking for all files listed in
rzk.yaml, with a progress indicator.
- Automatic code formatting on save (can be disabled via the
rzk.format.enable setting).
- Code navigation across the project: hover, go to definition and references, and workspace symbol search (CTRL + T on Windows/Linux, ⌘ + T on macOS).
See Changelog for recent updated and changes.
More examples:
Typechecking
The extension typechecks files in the open project automatically and reports all errors as diagnostic messages.
To define a Rzk project, simply create a file called rzk.yaml (not .yml!) that lists all the files to be typechecked under the include field. All paths are relative to the project root and support wildcards (for supported operators, see glob).
For example, a typcial rzk.yaml would look like so:
include:
- 'src/**/*.rzk'
- 'src/**/*.rzk.md'
Typechecking takes place automatically once the project is first opened and upon saving changes to any of the source files or the configuration file.
Configuration
Extension settings can be configured by going to the settings page (using the menu File > Preferences > Settings, or using the shortcut CTRL + , on Windows/Linux or ⌘ + , on macOS).
The currently available settings are:
| Name |
Type |
Default value |
Description |
rzk.path |
string |
"" |
The path to the rzk executable to use for the language server. "" (default) means that rzk executable available in PATH will be used. Takes precedence over rzk.manageInstallation. |
rzk.manageInstallation |
string |
"auto" |
Whether the extension should install and update its own copy of rzk. "auto" installs rzk only when it cannot be found on the system; "always" uses an extension-managed (automatically updated) rzk even when rzk is available in PATH; "never" never downloads rzk. |
rzk.fetchPrereleases |
boolean |
false |
If true, will include releases marked as "pre-release" on GitHub when fetching the latest binaries. |
rzk.format.enable |
boolean |
true |
Enable the Rzk formatter (provided via LSP). Disable to opt out of formatting on save. |
rzk.updateCheckIntervalMinutes |
number |
60 |
How often (in minutes) to check GitHub for new releases of rzk. Only applies to extension-managed installations; set to 0 to disable periodic checks. You can always trigger a check via the Rzk: Check for updates command. |
