Lean LSP MCP

by oOo0oOo

Overview Schema Source Related Servers Discussions Admin

Python

Hybrid

lean_diagnostic_messages

Read-onlyIdempotent

Get compiler errors, warnings, and infos for Lean files to diagnose and fix code issues.

Instructions

Get compiler diagnostics (errors, warnings, infos) for a Lean file.

Input Schema

TableJSON Schema

Name	Required	Description
`end_line`	No	Filter to line
`severity`	No	Filter by severity level. Returns all levels when omitted.
`file_path`	Yes	Absolute or project-root-relative path to Lean file
`timeout_s`	No	Max seconds to wait for elaboration. On timeout returns partial=true with still_elaborating_lines - poll again. Omit to wait for full elaboration.
`start_line`	No	Filter from line
`interactive`	No	Returns verbose nested TaggedText with embedded widgets. Only use when plain text is insufficient. For 'Try This' suggestions, prefer lean_code_actions.
`declaration_name`	No	Filter to declaration (slow)

Output Schema

TableJSON Schema

Name	Required	Description	Default
`result`	Yes

Schema Changelog

Changes observed during successful MCP inspections.

Changed3 schema fields changedv0.31.0Oct 3, 2026

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"
+}

Changed2 schema fields changedv0.29.0Jul 31, 2026

removedInput schema / properties / severity / anyOf

Removed value: -[
-  {
-    "enum": [
-      "error",
-      "warning",
-      "info",
-      "hint"
-    ],
-    "type": "string"
-  },
-  {
-    "type": "null"
-  }
-]

addedInput schema / properties / severity / enum

Added value: +[
+  "error",
+  "warning",
+  "info",
+  "hint"
+]

Changed8 schema fields changedv0.28.0Jul 11, 2026

removedInput schema / $defs

Removed value: -{
-  "DiagnosticSeverity": {
-    "enum": [
-      "error",
-      "warning",
-      "info",
-      "hint"
-    ],
-    "title": "DiagnosticSeverity",
-    "type": "string"
-  }
-}

changedInput schema / properties / severity / anyOf

Previous value: -[
-  {
-    "$ref": "#/$defs/DiagnosticSeverity"
-  },
-  {
-    "type": "null"
-  }
-]New value: +[
+  {
+    "enum": [
+      "error",
+      "warning",
+      "info",
+      "hint"
+    ],
+    "type": "string"
+  },
+  {
+    "type": "null"
+  }
+]

addedInput schema / properties / severity / title
```
Added value: +"Severity"
```
addedInput schema / properties / severity / type
```
Added value: +"string"
```

addedInput schema / properties / timeout_s

Added value: +{
+  "anyOf": [
+    {
+      "minimum": 1,
+      "type": "number"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Max seconds to wait for elaboration. On timeout returns partial=true with still_elaborating_lines - poll again. Omit to wait for full elaboration.",
+  "title": "Timeout S"
+}

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"
+}

addedOutput schema / $defs / DiagnosticsResult / properties / partial

Added value: +{
+  "default": false,
+  "description": "True when elaboration was still running at timeout: items may be incomplete and still_elaborating_lines shows the pending region. Poll again instead of treating this as failure.",
+  "title": "Partial",
+  "type": "boolean"
+}

addedOutput schema / $defs / DiagnosticsResult / properties / still_elaborating_lines

Added value: +{
+  "anyOf": [
+    {
+      "items": {
+        "items": {
+          "type": "integer"
+        },
+        "type": "array"
+      },
+      "type": "array"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Line ranges [start, end] (1-indexed) still being elaborated",
+  "title": "Still Elaborating Lines"
+}

Addedv0.10.0May 1, 2026
Removedv0.23.1May 1, 2026
First observedJan 26, 2026

TDQS

B3.3/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, so the safety profile is covered. The description adds the diagnostic categories (errors, warnings, infos) but says nothing about elaboration behavior, timeouts, or polling, which is where the real behavioral nuance lives (and is carried by the schema instead).

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 tight sentence with the core action front-loaded and no wasted words. Nothing redundant.

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?

An output schema exists, so return values need no explanation, and the schema covers all parameters. However, for a tool with 7 parameters and non-trivial elaboration/polling behavior, the description is thin on the when-and-why, leaving the agent to reconstruct context from structured fields alone.

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%, so every one of the 7 parameters is already documented (severity enum, timeout polling behavior, line filters, interactive widget caveat). The description adds no parameter detail beyond the schema, so baseline 3 applies.

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 (Get) and resource (compiler diagnostics) scoped to a Lean file, which is clear on its own. It does not distinguish this tool from siblings like lean_goal, lean_hover_info, or lean_code_actions, which also surface Lean analysis.

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?

There is no guidance on when to use this tool versus the many sibling diagnostics/analysis tools, nor any prerequisite or exclusion stated. The agent must infer usage entirely from the name.

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