✏️ lapis

A minimal, lightweight Language Server Protocol (LSP) framework in Lean 4.

This is just a scaffold for building language servers in Lean 4. It provides the core LSP protocol handling, a virtual file system (VFS) for managing text documents, and utilities for common LSP tasks.

🎨 Usage

Add lapis as a dependency in your lakefile.toml:

[[require]]
name = "lapis"
git = "https://github.com/SrGaabriel/lapis"
rev = "main"

💡 Example

This is a small example of a language server using lapis:

def main : IO Unit := do
  let config := LspConfig.new "example-server"
    |>.withVersion "0.1.0"
    |>.withCapabilities {
      textDocumentSync := some {
        openClose := some true
        change := some .full
        save := some { includeText := some false }
      }
      hoverProvider := some true
      completionProvider := some {
        triggerCharacters := some #["."]
        resolveProvider := some false
      }
    }
    |>.onRequestOpt "textDocument/hover" handleHover
    |>.onRequest "textDocument/completion" handleCompletion
    |>.onNotification "textDocument/didOpen" handleDidOpen
    |>.onNotification "textDocument/didChange" handleDidChange

  runStdio config
  
def handleDidOpen (ctx : RequestContext TestState) (params : DidOpenTextDocumentParams) : IO Unit := do
  ctx.showInfo "Document opened!"
  updateDiagnostics ctx params.textDocument.uri

📝 Features

Core Protocol

• Complete JSON-RPC 2.0 implementation
• LSP 3.17 base types (Position, Range, Location, Diagnostic, etc)
• Bidirectional messaging
• Request cancellation support
• Async request handling

Transport

• stdio transport (standard LSP communication)
• Thread-safe message output channel
• Proper Content-Length framing

Server Infrastructure

• Type-safe handler registration
• Clean ServerM monad for server operations
• Built-in document synchronization (open/change/close)
• User-defined state management
• Server and client capability negotiation

Virtual File System (VFS)

• Efficient finger tree-based text representation
• Piece table for fast incremental edits
• Line index with dirty range tracking
• UTF-8/UTF-16 position conversion for LSP compatibility
• Document snapshots with reference counting
• Thread-safe document store with IO-based operations
• O(log n) split/concatenation, O(1) amortized cons/snoc

Implemented LSP Features

• initialize / shutdown / exit lifecycle
• Text document synchronization (full and incremental)
• Hover (textDocument/hover)
• Completion (textDocument/completion)
• Go to definition (types defined, handler registration supported)
• Find references (types defined, handler registration supported)
• Publish diagnostics (textDocument/publishDiagnostics)
• Workspace configuration (workspace/configuration)
• Configuration change notifications (workspace/didChangeConfiguration)

Developer Experience

• Automatic JSON serialization/deserialization
• Type-safe message handlers with compile-time checks
• Helper methods for common operations (logging, messages, diagnostics)
• Generic configuration support for type-safe settings
• Builder pattern for server configuration

Concurrency

• Actor-based concurrency model with message passing
• Separate VFS and LSP actors for parallelism
• Per-request cancellation tokens
• Async request processing with bounded concurrency
• Thread-safe channels (unbounded, bounded, oneshot)
• Document snapshots with reference counting for concurrent access
• Actor supervision and lifecycle management

Server Utilities

• Progress reporting API with token lifecycle management
• Workspace edit support (workspace/applyEdit) with builder pattern
• Debounced diagnostics with per-document scheduling
• Dynamic capability registration (client/registerCapability)
• File watcher registration helpers