LSP Integration

How Astrolabe integrates with Lean's Language Server for real-time semantic information.

Astrolabe integrates with Lean 4's Language Server Protocol (LSP) to provide real-time semantic information, including proof status, diagnostics, and namespace discovery.

Architecture

Lean Project
    ↓
lake env lean --server  (LSP Server)
    ↓
LeanLSPClient (Python/AsyncIO)
    ↓
LSP Cache (.astrolabe/lsp.json)
    ↓
Frontend (Real-time visualization)

When Astrolabe connects to a Lean project, it spawns the Lean language server and communicates via the standard LSP protocol.

Features

Proof Status Detection

Astrolabe detects the proof status of each declaration:

Status is inferred from LSP diagnostics by matching them to symbol ranges.

Diagnostic Collection

The LSP server sends diagnostics as you edit Lean files:

{
  "severity": 1,
  "message": "unsolved goals\n⊢ n + 0 = n",
  "range": {
    "start": {"line": 45, "character": 10},
    "end": {"line": 45, "character": 20}
  }
}

Severity levels:

• 1: Error (compilation failure)
• 2: Warning
• 3: Information
• 4: Hint

Namespace Discovery

Astrolabe builds a namespace index from two sources:

1. Explicit namespaces: Found via namespace Foo declarations
2. Implicit namespaces: Extracted from definitions like def Foo.Bar.baz

The namespace index maps qualified names to file locations, enabling quick navigation.

Document Symbols

The LSP provides hierarchical symbol information:

{
  "name": "Nat.add",
  "kind": 12,
  "range": {
    "start": {"line": 41, "character": 0},
    "end": {"line": 50, "character": 0}
  },
  "children": [...]
}

Symbol kinds:

• 2 = Module
• 3 = Namespace
• 5 = Class
• 12 = Function
• 23 = Structure

Status Matching Algorithm

When multiple diagnostics exist, Astrolabe matches them to the innermost symbol:

def match_diagnostic_to_symbol(diagnostic, symbols):
    # Find the deepest symbol whose range contains the diagnostic
    # This handles nested declarations correctly

    for symbol in depth_first_traversal(symbols):
        if symbol.range.contains(diagnostic.range):
            return symbol

    return None  # File-level diagnostic

Status priority:

1. Error diagnostics → "error"
2. Sorry diagnostics → "sorry"
3. No issues → "proven"

Real-time Updates

File Watching

Astrolabe watches for changes to:

• .lean files → Triggers LSP re-analysis
• .ilean files → Triggers graph cache refresh

Status Sync

LSP status takes precedence over cached status:

def get_effective_status(node_id):
    lsp_status = lsp_cache.get_status(node_id)
    if lsp_status:
        return lsp_status
    return graph_cache.get_status(node_id)

This ensures the visualization reflects the latest proof state.

API Endpoints

Get Namespace Index

GET /api/project/namespace-index

Returns the cached namespace index from lsp.json.

Response:

{
  "namespaces": {
    "Nat": {
      "name": "Nat",
      "file_path": "/path/to/Nat.lean",
      "line_number": 10
    }
  }
}

Build Namespace Index

POST /api/project/namespace-index/build

Rebuilds the namespace index by querying the LSP server.

List Namespaces

GET /api/project/namespaces

Returns all discovered namespaces.

Refresh Namespaces

POST /api/project/namespaces/refresh

Forces a refresh of namespace information.

Find Declaration Namespace

GET /api/project/namespace-declaration?name=Nat.add

Finds which namespace contains a given declaration.

LSP Cache Structure

The lsp.json file caches LSP information to avoid repeated queries:

{
  "version": 3,
  "built_at": "2026-02-01T16:00:00Z",
  "files": {
    "/path/to/File.lean": {
      "symbols": [
        {
          "name": "MyTheorem",
          "kind": 12,
          "range": {...},
          "children": [...]
        }
      ],
      "diagnostics": [
        {
          "severity": 3,
          "message": "declaration uses 'sorry'",
          "range": {...}
        }
      ],
      "node_statuses": {
        "MyTheorem": "sorry"
      }
    }
  },
  "namespaces": {...}
}

Connection Lifecycle

Startup

1. Astrolabe spawns lake env lean --server
2. Sends LSP initialize request
3. Opens relevant .lean files
4. Collects symbols and diagnostics

During Use

• File changes trigger incremental updates
• Diagnostics are collected via textDocument/publishDiagnostics
• Status updates propagate to the visualization

Shutdown

• Sends LSP shutdown request
• Terminates the server process
• Caches final state to lsp.json

Retry Logic

The LSP client includes retry logic for reliability:

MAX_RETRIES = 10
RETRY_DELAY = 1.0  # seconds

async def get_document_symbols(file_path):
    for attempt in range(MAX_RETRIES):
        symbols = await lsp_client.request_symbols(file_path)
        if symbols:
            return symbols
        await asyncio.sleep(RETRY_DELAY)

    return []  # Timeout, return empty

This handles cases where Lean is still processing files.

Troubleshooting

LSP Connection Failed

To resolve:

1. Ensure lake build completes successfully
2. Check that Lean 4 is properly installed
3. Verify lake env lean --server works from terminal

Stale Status

If proof status seems outdated:

1. Save all Lean files
2. Wait for Lean to recompile
3. Use "Refresh" in Astrolabe or:

POST /api/project/namespace-index/build

Missing Symbols

If declarations are missing from the namespace index:

1. Ensure the file has been opened in Astrolabe
2. Check that lake build generated .ilean files
3. Rebuild the LSP cache:

POST /api/project/namespaces/refresh

Limitations

• LSP integration requires a successful lake build
• Large projects may have slower initial indexing
• Real-time updates depend on Lean's compilation speed
• Some complex diagnostics may not map precisely to symbols