Skip to main content
Glama
Sign In
Lean LSP MCP

Lean LSP MCP

by oOo0oOo
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Hybrid

lean_hover_info

Read-onlyIdempotent

Get type signature and documentation for a symbol at a given file line and column to understand Lean APIs.

Instructions

Get type signature and docs for a symbol. Essential for understanding APIs.

Input Schema

NameRequiredDescriptionDefault
lineYesLine number (1-indexed)
columnYesColumn at START of identifier (1-indexed characters)
file_pathYesAbsolute or project-root-relative path to Lean file

Output Schema

NameRequiredDescriptionDefault
infoYesType signature and documentation
symbolYesThe symbol being hovered
diagnosticsNoDiagnostics at this position

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. Changed2 schema fields changedv0.28.0
    • changedInput schema / properties / column / description
      Previous value: -"Column at START of identifier"New value: +"Column at START of identifier (1-indexed characters)"
    • 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.2/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 no behavioral context beyond that – no mention of build-state dependency or empty results on non-symbols. With annotations carrying the burden, this is minimally adequate.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two short sentences with the action front-loaded. The second sentence is somewhat generic ('Essential for understanding APIs') but costs little and stays brief.

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 not be explained, and annotations cover safety. Still, the description omits operational context such as needing an up-to-date build or what happens at non-symbol positions, leaving gaps for a tool whose results depend on file state.

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%, with line and column clearly documented as 1-indexed and column defined as the START of the identifier. The description adds no parameter meaning beyond the schema, so the 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?

States a specific verb and resource: 'Get type signature and docs for a symbol.' An agent can tell what it returns. However, it does not distinguish itself from closely related siblings like lean_completions, lean_goal, or lean_references, which also surface symbol information.

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?

The only guidance is 'Essential for understanding APIs,' which is a generic value claim rather than a when-to-use condition. It never says when to prefer this over siblings such as lean_completions or lean_references, nor any prerequisite (e.g. file must be built/loaded).

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