Skip to content
| Marketplace
Sign in
Visual Studio Code>Programming Languages>VioletNew to Visual Studio Code? Get it now.
Violet

Violet

Lîm Tsú-thuàn

|
1 install
| (0) | Free
Language support for the Violet dependently-typed proof assistant: LSP client (diagnostics, hover, goto-definition, references), semantic highlighting, unicode input, and snippets.
Installation
Launch VS Code Quick Open (Ctrl+P), paste the following command, and press enter.
Copied to clipboard
More Info

vscode-violet

VSCode extension for the Violet language. Provides syntax highlighting and acts as an LSP client to violet lsp.

Features

  • File association for .vt
  • TextMate grammar (keywords, comments, operators, strings, numbers)
  • Semantic tokens via the sibling tree-sitter-violet grammar — distinguishes let-defined names, data/record types, imported namespaces, and user-defined operator tokens
  • File icon for .vt
  • Unicode input picker — press \ in a .vt file to open a searchable picker showing each symbol (Π, Σ, λ, ∀, →, …) before you commit. Recently used symbols appear at the top. Type \\ to insert a literal backslash.
  • Keyword snippets — the same \ picker can insert Violet constructs (\let, \data, \record, …) that expand with interactive tab stops.
  • Language server features (via the violet CLI's lsp subcommand): diagnostics, goto-definition, hover, find references.

Language server

The extension launches violet lsp as a child process and talks JSON-RPC over stdio. Configure the binary path in your settings if violet isn't on your PATH:

"violet.serverPath": "/path/to/violet"

Other settings:

  • violet.lsp.enable (default true) — disable to skip starting the server.
  • violet.serverArgs (default ["lsp"]) — extra args passed to the binary.

Command: Violet: Restart Language Server restarts the server (e.g. after rebuilding the binary).

Unicode input

Press \ while editing a .vt file to open the unicode picker. Type a name (Pi, forall, to, lambda, …) or an alias to filter. Enter inserts the symbol at every cursor. Recently used symbols are pinned at the top.

To type a literal backslash, press \ twice: the first opens the picker, the second dismisses it and inserts a \.

Add your own mappings in settings:

"violet.unicodeInput.userSymbols": [
  { "name": "myop", "glyph": "⊕", "aliases": ["circplus"] }
]

A font with broad unicode coverage (e.g. JuliaMono, Fira Code, JetBrains Mono with Symbols Nerd Font) is recommended.

Keyword snippets

The same \ picker also lists Violet keyword snippets. Type a keyword to filter and select one to insert a construct that expands with interactive tab stops — press Tab to jump between fields. For example, data inserts:

\data Name : 𝓤
  | ctor : Name

with the cursor on Name first. Built-in snippets cover the keyword set (let, data, record, import, open, operator, where, elim, intro, split, fixity words, …).

Add your own snippets in settings (body uses VS Code snippet syntax):

"violet.snippetInput.userSnippets": [
  { "name": "lemma", "body": "\\let ${1:name} : ${2:Type} => ${0}", "detail": "lemma skeleton" }
]

Requirements

  • VSCode >= 1.85
  • For semantic tokens: nothing extra — the WASM grammar is bundled in the .vsix

Building from source

vscode-violet's build script reads the grammar from ../tree-sitter-violet.

npm install
npm run build:wasm    # requires emscripten or docker (used by tree-sitter-cli)
npm run compile
npm run package       # produces vscode-violet-<version>.vsix

Local install

code --install-extension vscode-violet-<version>.vsix

Development

Open vscode-violet/ in VSCode and press F5 to launch the Extension Development Host with the extension loaded.

Tests:

npm run test:grammar   # TextMate scope assertions
npm test               # semantic tokens smoke test (electron test runner)
  • Contact us
  • Jobs
  • Privacy
  • Manage cookies
  • Terms of use
  • Trademarks
© 2026 Microsoft