Lean LSP MCP Server

Was macht der “Lean LSP MCP”-Server?

Lean LSP MCP ist ein Model Context Protocol (MCP)-Server, der KI-Assistenten mit Lean Theorem Prover-Projekten über das Language Server Protocol (LSP) mittels des leanclient verbindet. Er ermöglicht Agenten und LLMs die Interaktion mit Lean-Projekten und bietet Zugriff auf Diagnosen, Zielzustände, Terminformationen, Hover-Dokumentation und mehr. Diese Integration rationalisiert Entwicklungs-Workflows für Lean-Anwender, indem ein umfangreiches, agentenorientiertes Toolset bereitgestellt wird, einschließlich Theoremsuche, Codevervollständigung und Projekt-Build-Funktionalität. Das Ziel des Servers ist es, die Arbeit von Entwicklern, Forschern und KI-Agenten mit Lean zu verbessern, indem Lean-Tools in automatisierten und interaktiven Kontexten zugänglich gemacht werden.

Liste der Prompts

Im Repository wurden keine Informationen zu Prompt-Vorlagen gefunden.

Liste der Ressourcen

Im Repository wurden keine Informationen zu bereitgestellten MCP-Ressourcen gefunden.

Liste der Tools

• Lean Theoremsuche: Ermöglicht Agenten die Suche nach Theoremen durch Integration von leansearch.net.
• Codevervollständigung: Bietet Codevervollständigungsvorschläge für Lean-Dateien.
• Projekt-Build: Erleichtert Projekt-Builds über das Lean-Buildsystem.
• Diagnosen: Bietet Zugriff auf Diagnosen innerhalb von Lean-Projekten.
• Zielzustände & Terminformationen: Stellt Zielzustände und Terminformationen für tiefere Projektanalysen bereit.
• Hover-Dokumentation: Gibt Dokumentation zurück, wenn Sie mit der Maus über Lean-Code-Elemente fahren.

Anwendungsfälle dieses MCP-Servers

• Lean-Projekt-Diagnosen: Sofortiger Zugriff auf Diagnosen zur Codekorrektheit und zum Debugging in Lean-Projekten.
• Erforschung von Zielzuständen: Abrufen und Anzeigen aktueller Zielzustände für die Beweisentwicklung und Strategieplanung.
• Theoremsuche: Relevante Theoreme über leansearch.net zur Unterstützung beim Beweisaufbau suchen.
• Codevervollständigung für Lean: Intelligente Codevervollständigung und Vorschläge für Lean bereitstellen, um die Produktivität zu steigern.
• Automatisierte Projekt-Builds: Lean-Projekt-Builds im Rahmen automatisierter Workflows oder agentischer Code-Reviews auslösen und überwachen.

Einrichtung

Windsurf

1. Stellen Sie sicher, dass uv installiert ist.
2. Bauen Sie Ihr Lean-Projekt, indem Sie lake build in Ihrem Projektverzeichnis ausführen.
3. Finden Sie die Windsurf-Konfigurationsdatei.
4. Fügen Sie den Lean LSP MCP-Server mit folgendem JSON-Snippet hinzu:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

5. Speichern Sie und starten Sie Windsurf neu. Überprüfen Sie, dass der MCP-Server läuft.

Claude

1. Installieren Sie uv und führen Sie lake build in Ihrem Lean-Projekt aus.
2. Öffnen Sie die Konfigurationsdatei von Claude.
3. Fügen Sie die MCP-Server-Konfiguration ein:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Speichern Sie und starten Sie Claude neu. Überprüfen Sie, dass der Server verfügbar ist.

Cursor

1. Installieren Sie uv und führen Sie lake build aus.
2. Öffnen Sie die Cursor-Konfigurationsdatei.
3. Fügen Sie den Lean LSP MCP-Server hinzu:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Speichern Sie die Änderungen und starten Sie Cursor neu.

Cline

1. Stellen Sie sicher, dass uv installiert ist, und führen Sie lake build aus.
2. Finden und bearbeiten Sie die Cline-Konfigurationsdatei.
3. Fügen Sie den Server hinzu:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. Speichern und starten Sie Cline neu.

API-Schlüssel sicher speichern

Falls Ihr Setup API-Schlüssel benötigt, verwenden Sie Umgebungsvariablen, um sie sicher zu speichern. Beispiel:

{
  "mcpServers": {
    "lean-lsp-mcp": {
      "command": "lean-lsp-mcp",
      "args": [],
      "env": {
        "API_KEY": "${env:LEAN_LSP_MCP_API_KEY}"
      },
      "inputs": {
        "api_key": "${env:LEAN_LSP_MCP_API_KEY}"
      }
    }
  }
}

Nutzung dieses MCP in Flows

MCP in FlowHunt verwenden

Um MCP-Server in Ihren FlowHunt-Workflow zu integrieren, fügen Sie zunächst die MCP-Komponente in Ihren Flow ein und verbinden Sie sie mit Ihrem KI-Agenten:

Klicken Sie auf die MCP-Komponente, um das Konfigurationspanel zu öffnen. Im Abschnitt zur systemweiten MCP-Konfiguration geben Sie Ihre MCP-Serverdetails in folgendem JSON-Format ein:

{
  "lean-lsp-mcp": {
    "transport": "streamable_http",
    "url": "https://yourmcpserver.example/pathtothemcp/url"
  }
}

Nach der Konfiguration kann der KI-Agent diesen MCP als Tool mit Zugriff auf alle Funktionen und Möglichkeiten verwenden. Denken Sie daran, “lean-lsp-mcp” durch den tatsächlichen Namen Ihres MCP-Servers zu ersetzen und die URL Ihrer eigenen MCP-Server-URL anzupassen.

Übersicht

Basierend auf der verfügbaren Dokumentation und dem Code bietet Lean LSP MCP starke Tool-Unterstützung für Lean-Projekte, es fehlen jedoch explizite Prompt-Vorlagen und MCP-Resource-Definitionen. Sampling- und Roots-Unterstützung werden nicht erwähnt. Insgesamt ist der Server für Lean-Nutzer praktisch, bietet aber noch nicht das gesamte Spektrum fortgeschrittener MCP-Funktionen.

MCP-Bewertung