Skip to content

rzk-lang/vscode-rzk

Folders and files

NameName
Last commit message
Last commit date
Sep 27, 2023
Jul 8, 2023
Jun 11, 2023
Jun 20, 2023
Dec 8, 2023
Apr 2, 2024
Jun 15, 2023
Jul 8, 2023
Dec 8, 2023
Mar 21, 2023
Nov 2, 2023
Jun 8, 2023
Oct 17, 2023
Dec 8, 2023
Dec 8, 2023
Sep 22, 2023
Jul 4, 2023

Repository files navigation

Supporting Rzk in VSCode (rzk-1-experimental-highlighting)

Visual Studio Marketplace Version (including pre-releases) Open VSX Version

Syntax and semantic highlighting for rzk, an experimental proof assistant for synthetic ∞-categories, as well as automatic typechecking.

Syntax highlighting example.

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:

Syntax highlighting example.

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.
rzk.fetchPrereleases boolean false If true, will include releases marked as "pre-release" on GitHub when fetching the latest binaries.