hol-lsp-mcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| HOL_BIN | No | The `hol` executable | $HOLDIR/bin/hol, else ~/HOL/bin/hol |
| HOL_LSP_EXTRA_PATH | No | Prepended to `PATH` for the server processes (e.g. `~/.local/polyml/bin`) | |
| HOL_LSP_MCP_MAX_SERVERS | No | How many servers may run at once. Each one holds a HOL heap. | 3 |
| HOL_LSP_GOALSTATE_BUDGET_MS | No | Passed to the servers: how long (ms) HOL may spend walking a tactic for `goalState`. HOL's own default, 1500, is too short for slow tactics such as CF's `xmatch`; HOL ignores the variable before its `lsp-walker-budget` patch (see `docs/upstream-issues.md`). | 10000 |
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {
"listChanged": false
} |
| prompts | {
"listChanged": false
} |
| resources | {
"subscribe": false,
"listChanged": false
} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| diagnosticsA | textDocument/publishDiagnostics + $/proofStates: a one-line verdict,
the proof tally and the diagnostics. Returns once the compile has
finished and no proof is still checking, or after |
| goalStateC | $/hol/goalState: the goal state at a position inside Proof ... QED. |
| evalA | $/eval: compile and run SML in the file's server process. Bindings are not echoed: use print or PolyML.print. Sees loaded theories/libraries, not the file's own declarations; changes persist in the process. |
| hoverC | textDocument/hover: type, value and documentation of the identifier. |
| definitionC | textDocument/definition: where the identifier is defined (path:line:column). |
| referencesC | textDocument/references (says so if the server does not support it; current HOL does not). |
| documentSymbolB | textDocument/documentSymbol: the file's outline (works even if it does not compile). |
| workspaceSymbolC | workspace/symbol in this file's server: stored theorems matching a substring (>= 2 chars). |
| completionC | textDocument/completion: names in scope and theorem names (first 50). |
| retryCompileC | $/hol/retryCompile: compile a file blocked on a missing dependency again. |
| restartA | Restart this file's server (e.g. after its dependencies were rebuilt,
or when diagnostics reports a probably looping proof). |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 11 tools
Each tool targets a clearly distinct operation: diagnostics for compile/proof status, goalState for interactive proof goals, eval for running SML, and standard LSP tools for hover, definition, references, symbols, and completion. retryCompile and restart are also distinguishable by context (retry a blocked file vs. restart the server). No two tools appear to do the same thing.
Names follow a consistent lowerCamelCase convention for multi-word tools (goalState, documentSymbol, workspaceSymbol, retryCompile) and single lowercase words elsewhere (diagnostics, eval, hover, definition, references, completion, restart). There is minor semantic variation between noun-style LSP names and verb-style action names, but no mixing of casing or separator styles.
11 tools is well-scoped for an LSP server focused on HOL theorem proving. The set covers core language intelligence (hover, definition, symbols, completion), HOL-specific interactions (diagnostics, goalState, eval), and recovery operations (retryCompile, restart) without redundancy.
The surface covers the main LSP capabilities an agent needs for HOL files, including compile diagnostics, proof goal inspection, evaluation, symbol search, and recovery. Minor gaps exist: references is documented as unsupported, and there is no direct tactic application or rename/code-action support, but agents can work around these by editing files and recompiling.