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).
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| line | Yes | ||
| column | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full behavioral burden. It does disclose a useful trait — results are capped at the first 50 — but omits whether this is read-only, what happens on out-of-range positions, error behavior, and the exact return shape. The cap disclosure is genuine added value but far from complete.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single compact sentence, front-loaded with the method name and the key content qualifier. Nothing is wasted, though the extreme terseness comes at the cost of the missing detail noted elsewhere.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no annotations, no output schema, and 0% parameter coverage, the description is too thin for a three-parameter tool standing among ten siblings. It should at least clarify the position semantics and how it differs from symbol-lookup tools.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0% and there are three required parameters (file, line, column). The description never explains what these mean or how they interact, e.g. that line/column denote a cursor position (and whether zero- or one-based). The names are largely self-evident, which prevents a 1, but the description adds nothing.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description names an LSP method (textDocument/completion) and states the returned content: names in scope and theorem names. That is more specific than a tautology, but it uses a noun ('completion') rather than a clear verb and does not distinguish this from siblings like documentSymbol or workspaceSymbol, which also surface symbols/names. An agent gets the gist but must infer the action.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No statement of when to use this tool versus the many siblings, and no exclusions or context. The agent is left to guess whether completion, documentSymbol, or workspaceSymbol is appropriate for a given lookup. Only the implicit LSP convention hints at usage.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
textDocument/definition: where the identifier is defined (path:line:column).
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| line | Yes | ||
| column | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full behavioral burden, and it does disclose the return format (path:line:column). However, it says nothing about the input position semantics, error behavior when no definition exists, or whether the file must be open, leaving clear gaps.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single tight sentence with the operation front-loaded and the result format appended. It earns its space but is terse to the point of under-specification.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
No annotations, no output schema, and three completely undocumented parameters leave the definition too thin to invoke reliably. The return-format hint helps but does not cover input semantics or edge cases.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% across three required parameters (file, line, column), so the description must compensate and largely does not. It implies line/column matter but only via the return format string, not by explaining that these identify the cursor position of the identifier.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific action (finding where an identifier is defined) and its output shape (path:line:column), which is clearer than a bare name. It does not explicitly distinguish itself from the sibling `references`, which is the inverse operation, so it stops short of a 5.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description says what the tool returns but nothing about when to use it versus alternatives. The sibling `references` (find all usages) is the obvious counterpart, and no when-to-use or exclusion guidance is offered.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.)
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| wait | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the burden well: it discloses the completion condition (compile finished and no proof still checking), the timeout behavior returning INCOMPLETE plus per-proof elapsed time, and that 'nothing is cancelled'. It also warns that long calls may be backgrounded past ~2 minutes. It stops short of stating that this is a non-mutating read, but the operational semantics are unusually well covered.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Dense but front-loaded: the return contents come first, then timing/incompleteness semantics, then the non-cancellation note. The LSP message names add jargon but also precision. Nothing is obviously padded, though the third sentence's parenthetical could be trimmed.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a two-parameter, no-output-schema tool, the description covers the return shape, timing, timeout, and incompleteness semantics an agent needs to interpret results. Gaps remain on the `file` argument's expected format and on how this relates to retryCompile/goalState, but the core calling contract is present.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% for both parameters. The description gives real meaning to `wait` — it is a timeout after which INCOMPLETE is returned — which is the non-obvious parameter. It adds nothing about `file` (format, relative vs absolute path), leaving that purely to the schema name.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States the specific outputs — a one-line verdict, the proof tally, and diagnostics — tied to the defining LSP messages (textDocument/publishDiagnostics + $/proofStates). It is clear what the tool returns, but it never contrasts itself with the closest sibling, goalState, which likely overlaps in proof-state information, so an agent must still guess which to call.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied: call it to get compile diagnostics/proof states, and 'call again to keep waiting' gives an actionable retry pattern. However, there is no explicit when-to-use versus alternatives such as goalState, retryCompile, or restart, so the agent gets no routing guidance between siblings.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
textDocument/documentSymbol: the file's outline (works even if it does not compile).
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It does disclose one genuinely useful trait, that it works even when the file does not compile, but says nothing about the returned structure, ordering, or whether results are cached or truncated.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single front-loaded sentence that identifies the method and its scope, followed by a parenthetical qualifier. No wasted words.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a one-parameter read tool this is close to adequate, but with no output schema the description should say something about what an outline contains (nested symbols with kinds and ranges) so the agent can plan on consuming the result.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% and the single 'file' parameter is undocumented anywhere. The description does not clarify whether the value is a filesystem path, an absolute path, or a URI, which is exactly the ambiguity that breaks LSP-style calls.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific resource and result: 'the file's outline,' with the canonical LSP method name. It is distinguishable from workspaceSymbol (file scope vs workspace scope), though the description never names that sibling explicitly.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied by the phrase 'the file's outline' and the qualifier that it works even on non-compiling files, which hints at when it is preferable to diagnostics. There is no explicit when-to-use or when-to-prefer-a-sibling guidance.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
$/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.
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | ||
| file | Yes | ||
| timeout | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full behavioral burden and does notable work: it discloses that bindings are not echoed (use print/PolyML.print), that evaluation scope excludes the file's own declarations, and that state changes persist in the server process. This surfaces real side effects and output semantics. It stops short of covering failure modes, timeout behavior, or what happens to a hung evaluation.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Three tightly packed sentences, front-loaded with the action, then output behavior, then scope/persistence caveats. No filler and every clause carries information an agent needs.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a stateful code-execution tool with no annotations, no output schema, and 0% parameter documentation, the description covers purpose and key semantics but leaves the timeout parameter, error/timeout behavior, and result shape unexplained. Adequate but with clear gaps.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% and all three properties are bare (title only). The description only loosely implies that 'file' selects the server process and 'code' is the SML to run; 'timeout' is never addressed despite defaulting to 120. It does not compensate for the coverage gap.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a precise verb pair (compile and run) and resource (SML in the file's server process), which cleanly separates it from sibling compile/retry tools like retryCompile and from read-only inspection tools like diagnostics. An agent can tell what this tool does without opening the schema.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied by the mechanics ('compile and run SML') rather than stated as a when-to-use rule; no alternative is named and no condition for choosing this over retryCompile or diagnostics is given. The environmental notes ('sees loaded theories/libraries, not the file's own declarations') helpfully bound when results are meaningful, but that is guidance by inference.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
$/hol/goalState: the goal state at a position inside Proof ... QED.
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| line | Yes | ||
| column | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full behavioral burden. It does not state what is returned (raw goal text, structured goals, error when outside a proof), whether the position must be inside a checked region, or any timing/state requirements, leaving significant gaps for a proof-assistant query tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single fragment that is arguably too terse rather than concise; the 'Proof ... QED' ellipsis obscures rather than clarifies. There is no front-loaded statement of what the tool returns, so the brevity costs comprehension.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no annotations, no output schema, and three fully undocumented parameters, the description would need to explain return shape and preconditions. It instead supplies only a fragmentary resource name, leaving the agent without enough context to invoke the tool confidently.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% across three required parameters (file, line, column), so the description must compensate. 'At a position' loosely maps to the line/column/file triple, but it adds no detail on path format, 0- vs 1-based indexing, or whether line/column refer to the proof file's coordinates.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description names the resource ('goal state at a position inside Proof ... QED'), which conveys that it retrieves proof-state information for a source location. However, it lacks a clear verb and the 'Proof ... QED' ellipsis is cryptic, so an agent must infer it means 'within a proof block'. It does not differentiate itself from sibling tools like hover or diagnostics that also operate on a file position.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The phrase 'inside Proof ... QED' is the only hint of applicability, implying the tool is only meaningful within a proof context, but there is no explicit when-to-use, prerequisites, or pointer to alternatives. The agent gets no guidance on how this differs from hover or diagnostics for the same position.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
textDocument/hover: type, value and documentation of the identifier.
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| line | Yes | ||
| column | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full behavioral burden. It implies a read-only lookup but never states that it has no side effects or mutations, nor whether it requires the file to be open or compiled. Return format is only gestured at (type/value/documentation) with no structure or empty-result behavior.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single tight sentence with the payload front-loaded after the LSP method prefix. The 'textDocument/hover:' prefix is slightly redundant with the tool name but overall there is no waste.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
No annotations, no output schema, and three undocumented required position parameters mean the description must do the heavy lifting, and it falls short. Missing coordinate conventions and result-shape guidance make correct invocation a guess.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate, and it does not. It never explains that file/line/column locate the identifier, nor whether line and column are 0-based or 1-based — a critical ambiguity for an LSP position-based tool.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
Names a specific operation (hover) on a specific resource (an identifier at a position) and enumerates the returns: type, value, documentation. This distinguishes it reasonably from siblings like definition and references. It lacks explicit sibling contrast, which keeps it out of 5 territory.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
There is no statement of when to reach for hover rather than definition, references, or documentSymbol, and no preconditions such as requiring an open/analyzed document. The agent is left to infer usage from the name alone.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
textDocument/references (says so if the server does not support it; current HOL does not).
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| line | Yes | ||
| column | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full behavioral burden. It discloses an important trait — the tool will signal unsupported on servers without references support, and the current HOL server does not support it — but says nothing about return format, position conventions, or error behavior beyond that single case.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single compact sentence with the key caveat up front and no filler. The parenthetical is somewhat terse/cryptic, but nothing is wasted.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a three-parameter positional lookup with no annotations, no output schema, and no parameter documentation, the description is too thin — it never explains what the tool returns or how the position arguments are interpreted, leaving the agent reliant on outside LSP knowledge.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Three required parameters (file, line, column) with 0% schema description coverage, and the description adds no meaning for any of them — it never clarifies that line/column denote the symbol position or whether indexing is 0- or 1-based. It does not compensate for the coverage gap.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description largely restates the tool name by mapping it to the LSP method 'textDocument/references', without stating the actual action (e.g. 'find all references to the symbol at the given position'). An agent unfamiliar with LSP conventions gets no explicit verb-and-resource statement, and it is not distinguished from siblings like definition or hover.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It implicitly conveys usage via the LSP method name and, more usefully, warns that the tool reports unsupported when the server lacks it and that the current HOL server does not support it. However, it gives no guidance on when to prefer this over definition, hover, or workspaceSymbol.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| max_heap_mb | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden. It discloses the meaningful side effect that max_heap_mb 'sets this file's heap cap from now on', which is genuine behavioral context, but says nothing about what is lost when the server is torn down (in-memory proof state), whether the operation is disruptive, or its cost.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Purpose is front-loaded in the first clause, followed by trigger examples and then parameter semantics. Dense but every clause earns its place; no filler.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a two-parameter restart tool with no output schema and no annotations, the description covers purpose, triggers, and the non-obvious heap-cap semantics. The main gap is the absence of any statement about post-restart state or disruption, which an agent might want before calling it.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate. It explains max_heap_mb well — '0 for none' and that the server's configured cap applies by default — which is more than the bare integer schema conveys. The required 'file' parameter is only implied via 'this file', not explicitly described.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description names a specific verb and resource ('Restart this file's server') and gives two concrete trigger examples. It is clear on its own, but it never distinguishes itself from the closest sibling 'retryCompile', which an agent could easily confuse with a restart.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It provides clear when-to-use context: after dependencies were rebuilt, or when diagnostics reports a probably looping proof. That implies a diagnostics-first workflow, but no explicit when-not condition or named alternative is offered.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
$/hol/retryCompile: compile a file blocked on a missing dependency again.
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It discloses only the precondition (file blocked on a missing dependency) and that the compile is re-run; it says nothing about side effects such as emitted artifacts, whether it blocks until completion, what happens if the dependency is still missing, or what result is returned.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single, front-loaded sentence with no padding. The redundant protocol-method prefix costs a little, but the action and its precondition come first and the sentence ends immediately.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no annotations, no output schema, and an undocumented required parameter, the description should do more for a tool that triggers compilation. It leaves unresolved the path format, failure behavior, and result of the retry, which an agent needs before invoking it.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% for the single 'file' parameter, so the description must compensate and does not: it never says whether 'file' is an absolute path, a workspace-relative path, or a URI, nor whether it must be an already-open document. Only the vague notion that it is 'a file blocked on a missing dependency' is conveyed.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific action (compile again) on a specific resource (a file blocked on a missing dependency), which clearly separates it from the read-only navigation siblings (hover, definition, references, diagnostics). The '$/hol/retryCompile' prefix restates the tool name rather than adding information, but the verb+resource+precondition is unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The phrase 'blocked on a missing dependency' implies the triggering condition (retry after the dependency has been resolved), which is useful implicit guidance. However, it names no alternative tool, no exclusion (e.g., don't use for files that never compiled), and no prerequisite that the dependency now exists.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
workspace/symbol in this file's server: stored theorems matching a substring (>= 2 chars).
| Name | Required | Description | Default |
|---|---|---|---|
| file | Yes | ||
| query | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are supplied, so the description carries the full disclosure burden. It does add one genuine behavioral detail (the >= 2 character substring minimum), but says nothing about result limits, matching semantics (case sensitivity, fuzzy vs exact), or whether the search spans all open files.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single compact sentence with no filler, and the key constraint is placed immediately after the operation name. The terse 'workspace/symbol in this file's server' phrasing is a bit cryptic, but nothing is wasted.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
With no annotations, no output schema, two required parameters, and 0% schema description coverage, the description should do considerably more. It leaves the mandatory 'file' argument undefined and gives no sense of what a successful result looks like or how results are bounded.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0% and neither parameter has a schema description. The description partially compensates for 'query' by specifying substring matching and the 2-character floor, but the required 'file' parameter is never explained at all — an agent cannot tell whether it is the file to search within, the file providing context, or a file to exclude.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description names a concrete retrieval operation (finding stored theorems by substring) with a stated scope ('workspace/symbol'), which is more specific than a bare restatement. It does not, however, differentiate itself from sibling symbol tools such as documentSymbol or references, so an agent must infer the scope distinction from the word 'workspace' alone.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
There is no statement of when to use this tool versus documentSymbol, references, or definition, and no preconditions or exclusions. The only actionable guidance is the embedded substring rule (>= 2 chars), which is a constraint rather than usage routing.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v0.1.0completiondefinitiondiagnosticsdocumentSymbolevalgoalStatehoverreferencesrestartretryCompileworkspaceSymbolScored 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.
The official Svelte MCP server providing docs and autofixing tools for Svelte development
Official DevSpeak MCP server — translate technical text into formal specs from any AI IDE or agent
Shared control plane for AI coding agents — tasks, memory, decisions, file locks. 12 tools.
