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:

1. Basic syntax highlighting with a simple TextMate grammar.
2. Semantic highlighting via LSP (you must have rzk version v0.6 or above).
3. Prompts for installing/updating rzk binaries from GitHub Releases automatically (usable from local Terminal).
4. Markdown Preview button for *.rzk.md files.
5. Automatic typechecking for all files listed in rzk.yaml

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: