Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@hol-lsp-mcp check diagnostics for fooScript.sml"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
Status: experimental. This tool was written largely by an AI coding agent (Claude) and has not yet been reviewed by a human. Expect rough edges; use at your own risk.
Reviewed up to commit: none yet.
A small MCP server that lets coding agents
such as Claude Code use HOL4's built-in language server, bin/hol lsp.
The tools mirror the server's LSP methods one-to-one, with the same names and
meanings, so if you know hol lsp there is nothing new to learn. The wrapper
only adds what an agent can't easily do itself:
Server lifecycle. It runs one hol lsp --lsp-check-proofs process per
file, because the server serves only one script. Each process starts in the
file's directory, so it picks up that directory's Holmakefile and
HOLHEAP. Servers stay alive between calls. At most
HOL_LSP_MCP_MAX_SERVERS run at once, and the least recently used idle one
is shut down to make room. A server that has died is restarted on the next
call, and the response includes its stderr tail. All servers are shut down
when the MCP server exits.
File sync from disk. The agent edits files with its normal tools. Every
call re-reads the file and sends didOpen or a full-text didChange if the
file has changed.
Waiting for results, for as long as the agent chooses. diagnostics
waits for the compile of the current text to finish, then until no proof
is still checking and the server has been quiet for about a second. It
gives up after wait seconds (default 25) and says INCOMPLETE, but that
cancels nothing: the server carries on, and the next call picks up where
this one stopped. For each proof still checking it says how long the
wrapper has seen it checking (counted from the last edit at most), next to
how long the slowest finished proof in the file took, so that a looping
proof stands out. If the file hasn't changed since a settled answer, it
returns immediately. Other calls on the same file do not queue behind a
waiting diagnostics.
Memory and looping proofs: two limits. Poly/ML lets a process grow to
80% of RAM by default, so one looping proof can take the whole machine
(a server has been seen at 13 GB). The hard limit is Poly/ML's
--maxheap, given to every server: at the cap Poly/ML interrupts the
server's threads, so the proof fails with Interrupt, or, if Poly
cannot recover (Run out of store ... Failed to recover - exiting, as
seen with a looping rewrite under a 1500 MB cap), the server exits and
the next call restarts it. Either way the machine keeps its memory. The soft limits only report:
diagnostics says PROBABLY LOOPING: proof X (line N) has been checking for M, ...; server footprint G GB. Cancel it or restart? when a proof
has been checking for over 3 minutes, or for ten times as long as the
slowest finished proof (and at least a minute), and SERVER LARGE when
the server's footprint is over the soft limit. Nothing is ever stopped:
edit or cheat the proof to cancel it, or call restart. The footprint is
the physical footprint (compressed and swapped pages included), not RSS.
Positions. All lines and columns are 1-based, and columns count Unicode
characters, which is how an agent sees a file full of ∀, ⇒ and ‘’. The
wrapper negotiates utf-8 with the server and converts in both directions.
It handles utf-16 too.
Flagging cheat. The server's pool checks hypotheses, not oracle tags,
so it reports a proof that uses cheat as proved. diagnostics therefore
also scans the file text for cheat as a whole word, skipping comments and
string literals. If it finds any, the verdict is never OK: it reads
CHEATS: 2 proofs use cheat (foo, bar), and each use is listed with its
enclosing theorem and line.
Text output. Results are concise text written for an agent's context, not raw JSON.
tool | server method | returns |
|
| One-line verdict (never |
|
| theorem, step, context tags, note, error, goals ( |
|
| errors and warnings with positions in |
|
| the hover text |
|
|
|
|
|
|
|
| outline: line, name, kind, detail |
|
| name, kind, theory, location |
|
| labels with details, first 50 |
|
| sends the notification; call |
| (wrapper) | kills and restarts that file's server, e.g. after its dependencies were rebuilt; |
An unfinished answer looks like this:
INCOMPLETE after 25s: 48/50 proved, 2 still checking
The server keeps checking; call diagnostics again to keep waiting.
Proofs: 48 proved, 2 checking (50 total)
par_actions_cong (line 120): checking for 4m12s (finished proofs here took ≤3s)
freeze_agree (line 131): checking for 4m12s (finished proofs here took ≤3s)
Diagnostics: noneRelated MCP server: LSP MCP
You need Python 3.10 or later and a built HOL (bin/hol and bin/hol.state).
cd hol-lsp-mcp
python3 -m venv .venv
.venv/bin/pip install -e .Environment variables:
variable | default | meaning |
|
| the |
| unset | prepended to |
|
| how many servers may run at once. Each one holds a HOL heap. |
|
| hard limit: Poly/ML |
|
| soft limit: server footprint above which |
|
| soft limit: how long a proof may check before |
|
| idle shutdown: a server with no tool calls for this long is stopped, freeing its heap; the next call on the file starts a fresh one and says so in its reply. Not while a call is waiting on it or a proof is still checking (a probably-looping proof does not count). |
|
| passed to the servers: how long (ms) HOL may spend walking a tactic for |
Register it with Claude Code at local scope (the default scope):
claude mcp add hol-lsp \
-e HOL_BIN=$HOME/HOL/bin/hol \
-e HOL_LSP_EXTRA_PATH=$HOME/.local/polyml/bin \
-- $HOME/Programming/hol-lsp-mcp/.venv/bin/hol-lsp-mcp serveThe CLI uses the same core code. Each run starts a fresh server, so the
position-based commands first wait for the compile to finish (--no-wait
skips this).
.venv/bin/hol-lsp-mcp diagnostics path/to/fooScript.sml
.venv/bin/hol-lsp-mcp goalState path/to/fooScript.sml 42 5
.venv/bin/hol-lsp-mcp eval path/to/fooScript.sml 'PolyML.print (DB.find "ADD_COMM");'
.venv/bin/hol-lsp-mcp hover path/to/fooScript.sml 42 5
.venv/bin/hol-lsp-mcp workspaceSymbol path/to/fooScript.sml ADD_COMMhol lsp is HOL's own LSP server (see tools-poly/lsp/README.md and
Manual/Developers/lsp-server.md in the HOL tree). This project is a client
for it, like HOL's eglot and VS Code clients. As both of those do, it turns
proof checking on (--lsp-check-proofs), so the server's worker pool really
runs every proof after the fast elaboration pass.
Some server behaviour worth knowing:
One server per script. A server is pinned to the dependencies it loaded
first. After you rebuild a dependency with Holmake, call restart. A
dependency that was missing is re-read on retryCompile.
cheat is tallied as proved. The pool's verdict compares hypotheses,
not oracle tags, so replaying cheat succeeds. The wrapper's text scan,
described above, makes up for this. In the tally, cheated means "not being
checked": the proof was dropped by an edit, or its tactic didn't compile and
it is taken on trust.
The tally is accumulated from transitions. The server never retracts a
name, so the wrapper hides cheated entries whose name no longer appears in
the file. Otherwise deleted or renamed theorems would stay in the tally.
eval runs in the server process, not in the file's namespace: it sees
loaded theories and libraries, but not the file's own vals. It does not
echo bindings. PolyML.print output comes back in the reply, while print
output goes to the server's stderr, which the wrapper captures and appends.
The server's automatic holdep preloading may log harmless lines such as
Cannot find file PolyML.ui.
An edit that runs from one proof into the next used to leave the second
proof's old check running. The server decides from where an edit
starts whether it is confined to one proof. If it is, the server cancels
that proof's check and keeps the checks of the proofs below, matching them
by name. So if one write changed two proofs, the second one's old tactic
kept running, and if that tactic looped, the proof stayed checking
forever. The wrapper avoids this. When a change starts inside a proof body
and runs past its QED, it first sends a copy of the new text with a blank
line inserted before that declaration, then the real text. The server takes
the first as a statement edit and re-checks everything below. A fix for the
server is described in docs/upstream-issues.md.
Hover returns nothing on a line that contains a string literal with
non-ASCII characters, e.g. val p = ("∀", foo). This happens at every
offset on that line, so it isn't a position-conversion problem.
.venv/bin/python -m unittest discover -s tests # unit tests (no HOL needed)
.venv/bin/python tests/e2e_hol_lsp.py -v # against a real hol lspThe unit tests cover framing, position conversion, the cheat scan, and the
session and lifecycle logic against a fake server (tests/fake_hol_lsp.py),
including waiting without blocking other calls. The
end-to-end script skips cleanly if HOL isn't built. Set
HOL_LSP_E2E_VERBOSE=1 to see every tool's output.
BSD-3-Clause; see LICENSE.
textDocument/completion: names in scope and theorem names (first 50).
Inputs: file (required), line (required), column (required).
textDocument/definition: where the identifier is defined (path:line:column).
Inputs: file (required), line (required), column (required).
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 wait seconds with
INCOMPLETE and how long each unfinished proof has been checking.
Nothing is cancelled: call again to keep waiting. (Clients may move
calls longer than about two minutes to the background.)
Inputs: file (required), wait.
textDocument/documentSymbol: the file's outline (works even if it does not compile).
Inputs: file (required).
$/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.
Inputs: code (required), file (required), timeout.
$/hol/goalState: the goal state at a position inside Proof ... QED.
Inputs: file (required), line (required), column (required).
textDocument/hover: type, value and documentation of the identifier.
Inputs: file (required), line (required), column (required).
textDocument/references (says so if the server does not support it; current HOL does not).
Inputs: file (required), line (required), column (required).
Restart this file's server (e.g. after its dependencies were rebuilt,
or when diagnostics reports a probably looping proof). max_heap_mb
sets this file's heap cap from now on (0 for none); by default the
server's configured cap applies.
Inputs: file (required), max_heap_mb.
$/hol/retryCompile: compile a file blocked on a missing dependency again.
Inputs: file (required).
workspace/symbol in this file's server: stored theorems matching a substring (>= 2 chars).
Inputs: file (required), query (required).
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
Loading tool schema changelog…
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.
Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.
AI-native programming language and toolchain for accountable, verifiable agent-driven development.
The official Svelte MCP server providing docs and autofixing tools for Svelte development
Shared memory MCP server for Claude Code, Codex, Gemini CLI and Cursor. Cited, editable.
