Compile and run SML code in a file's HOL4 server process, using loaded theories and libraries. Print results explicitly; changes persist during the session.
$/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 |
Changes observed during successful MCP inspections.
v0.1.0Does 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.