Skip to main content
Glama
oOo0oOo

Lean LSP MCP

by oOo0oOo
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Hybrid

lean_run_code

Read-onlyIdempotent

Execute self-contained Lean code with all imports and return diagnostics, enabling agents to validate snippets and catch errors.

Instructions

Run a code snippet and return diagnostics. Must include all imports.

Input Schema

TableJSON Schema
NameRequiredDescriptionDefault
codeYesSelf-contained Lean code with imports

Output Schema

TableJSON Schema
NameRequiredDescriptionDefault
successYesWhether code compiled successfully
timed_outNoTrue if elaboration timed out (results are partial)
diagnosticsNoCompiler diagnostics

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed3 schema fields changedv0.31.0
    • addedOutput schema / $defs / DiagnosticCategory
      Added value: +{
+  "enum": [
+    "diagnostic",
+    "linter",
+    "sorry",
+    "suggestion"
+  ],
+  "title": "DiagnosticCategory",
+  "type": "string"
+}
    • addedOutput schema / $defs / DiagnosticMessage / properties / category
      Added value: +{
+  "$ref": "#/$defs/DiagnosticCategory",
+  "default": "diagnostic",
+  "description": "'linter' is style noise (unused variables and the like) that does not block compilation; 'sorry' marks an unproved declaration and is never noise; 'suggestion' carries a `Try this:` replacement; 'diagnostic' is everything else."
+}
    • addedOutput schema / $defs / DiagnosticMessage / properties / hint
      Added value: +{
+  "anyOf": [
+    {
+      "type": "string"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Guidance for a recognised failure mode, when one applies",
+  "title": "Hint"
+}
  2. Changed1 schema field changedv0.28.0
    • addedOutput schema / $defs / DiagnosticMessage / properties / lean_tags
      Added value: +{
+  "anyOf": [
+    {
+      "items": {
+        "type": "string"
+      },
+      "type": "array"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Lean-specific tags: 'unsolvedGoals' (proof incomplete here) or 'goalsAccomplished' (proof finished). Machine-readable proof status - prefer over string-matching the message.",
+  "title": "Lean Tags"
+}
  3. Addedv0.10.0
  4. Removedv0.23.1
  5. First observed

TDQS

B3.4/5.0
Behavior3/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare readOnlyHint=true, idempotentHint=true, and openWorldHint=false, covering safety and idempotency. The description adds the requirement to include all imports, which is useful behavioral information, but doesn't disclose other traits like execution limits, error handling, or output format. An output schema exists, so return values needn't be explained.

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?

Two short sentences with zero waste; the critical requirement is front-loaded and directly actionable.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given annotations that cover safety and idempotency, a single parameter with full schema coverage, and an output schema, the description is nearly complete. It could benefit from mentioning when to use this tool over similar siblings, but otherwise nothing essential is missing.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100% and there is only one parameter. The description's note to 'include all imports' reinforces the schema's description of 'code' as 'Self-contained Lean code with imports', but adds no new syntax or format details. Baseline 3 is appropriate when the schema fully documents the parameter.

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?

The description states a specific verb (Run) and resource (code snippet) and mentions returning diagnostics. However, it doesn't differentiate this tool from similar siblings like lean_build or lean_multi_attempt, which likely also execute code.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance is provided on when to use this tool versus alternatives such as lean_build or lean_multi_attempt. The only directive is a requirement ('Must include all imports'), which is a parameter constraint rather than usage context.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Deploy Server

Other Tools