Summit Breeze

An LSP server for SMT-LIB files, with a VS Code extension for syntax highlighting and language support.

Features

LSP Server (Rust)

Full SMT-LIB v2.6 parser with Z3 extension support
Go-to-definition — jump to declarations of functions, constants, sorts, variables, and local bindings (forall/exists/let)
Find references — scope-aware: only shows references to the specific definition under cursor
Hover — shows the source definition of a symbol
Push/Pop navigation — go-to-definition on push jumps to matching pop and vice versa
Document outline — structured view of declarations, assertions, push/pop blocks
Folding — fold top-level commands and push/pop blocks
Diagnostics — real-time parse error reporting
Error recovery — a single typo doesn't break the entire file
Scales to large files — hand-written lexer and parser optimized for throughput

VS Code Extension

Syntax highlighting for .smt2 and .smt files (TextMate grammar)
Automatic LSP server startup (bundled binary, no separate install needed)
Bracket matching, auto-closing pairs, and SMT-LIB-aware word selection
Configurable server path for development/debugging

Installation

From a Release (recommended)

Download the .vsix for your platform from the Releases page, then:

code --install-extension summit-breeze-<platform>-<version>.vsix

The extension bundles the LSP server binary — no additional setup required.

From Source

# Clone
git clone https://github.com/FStarLang/summit-breeze.git
cd summit-breeze

# Build and package the VSIX for your platform
./package.sh

# Install the resulting .vsix
code --install-extension editors/vscode/summit-breeze-*.vsix

Prerequisites

Rust 1.75+ (2024 edition)
Node.js 18+ (for the VS Code extension)

Development Setup

For development, you can skip the VSIX and run the LSP binary directly:

cargo build --release --bin summit-breeze-lsp

Then either add target/release/ to your PATH (the extension falls back to PATH lookup), or set the summitBreeze.serverPath setting in VS Code to the binary path.

Configuration

Setting	Description
`summitBreeze.serverPath`	Path to a custom `summit-breeze-lsp` binary. Leave empty to use the bundled binary.

Project Structure

summit-breeze/
├── crates/
│   ├── parser/          # smtlib-parser: lexer, AST, recursive descent parser
│   └── lsp/             # summit-breeze-lsp: LSP server binary
├── editors/
│   └── vscode/          # VS Code extension
└── package.sh           # Build + package script

Running Tests

# All tests
cargo test

# Parser tests only
cargo test -p smtlib-parser

# LSP + integration tests
cargo test -p summit-breeze-lsp

# Performance benchmark
cargo run --release --example bench -p smtlib-parser

Other Editors

The LSP server communicates over stdio. Configure your editor's LSP client to launch summit-breeze-lsp with stdio transport.

Supported SMT-LIB Commands

Category	Commands
Logic	`set-logic`, `set-info`, `set-option`
Declarations	`declare-fun`, `declare-const`, `declare-sort`, `define-fun`, `define-sort`
Z3 Extensions	`declare-datatype(s)`, `define-fun-rec`, `define-funs-rec`, `lambda`
Assertions	`assert`, `check-sat`, `check-sat-assuming`
Stack	`push`, `pop`, `reset`, `reset-assertions`
Model	`get-model`, `get-value`, `get-proof`, `get-unsat-core`
Other	`echo`, `exit`, and unknown commands (gracefully parsed)

Design Decisions

Single-file model: each document is independent — no cross-file references
Full reparse on edit: fast enough for large files with the hand-written parser
Error recovery: on parse error, skip to next balanced paren / next top-level command
Extensible grammar: unknown commands are parsed as generic s-expressions

License

Apache-2.0 — see LICENSE for details.