Skip to main content
Glama
briancmlee

hol-lsp-mcp

by briancmlee

documentSymbol

Get a file's symbol outline from HOL4 SML scripts, even when the file does not compile.

Instructions

textDocument/documentSymbol: the file's outline (works even if it does not compile).

Input Schema

TableJSON Schema
NameRequiredDescriptionDefault
fileYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv0.1.0

TDQS

B3.3/5.0
Behavior3/5

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.

Conciseness5/5

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.

Completeness3/5

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.

Parameters2/5

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.

Purpose4/5

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.

Usage Guidelines3/5

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.