Lean LSP MCP Server

Vad gör “Lean LSP MCP”-servern?

Lean LSP MCP är en Model Context Protocol (MCP)-server som kopplar AI-assistenter med Lean Theorem Prover-projekt via Language Server Protocol (LSP) med hjälp av leanclient. Den möjliggör för agenter och LLM:er att interagera med Lean-projekt och ger tillgång till diagnostik, måltillstånd, terminformation, hover-dokumentation och mer. Denna integrering effektiviserar utvecklingsflöden för Lean-användare genom att erbjuda en rik agentfokuserad verktygslåda, inklusive teoremsökning, kodkomplettering och projektbygge. Servern syftar till att förbättra upplevelsen för utvecklare, forskare och AI-agenter som arbetar med Lean genom att göra Leans verktyg tillgängliga i automatiserade och interaktiva sammanhang.

Lista över promptar

Ingen information om promptmallar hittades i arkivet.

Lista över resurser

Ingen information om exponerade MCP-resurser hittades i arkivet.

Lista över verktyg

• Lean Theorem Search: Låter agenter söka teorem genom integration med leansearch.net.
• Kodkomplettering: Ger förslag på kodkomplettering för Lean-filer.
• Projektbygge: Underlättar projektbyggen via Leans byggsystem.
• Diagnostik: Ger åtkomst till diagnostik inom Lean-projekt.
• Måltillstånd & terminformation: Exponerar måltillstånd och terminformation för djupare projektanalys.
• Hover-dokumentation: Returnerar dokumentation vid hovring över Lean-kodelement.

Användningsområden för denna MCP-server

• Lean-projektdiagnostik: Få direktåtkomst till och visa diagnostik för korrekthet och felsökning i Lean-projekt.
• Utforskning av måltillstånd: Hämta och visa aktuella måltillstånd för bevisutveckling och strategiplanering.
• Teoremsökning: Sök efter relevanta teorem från leansearch.net för att hjälpa till vid beviskonstruktion.
• Kodkomplettering för Lean: Ge intelligenta kodkompletteringar och förslag för Lean, vilket ökar produktiviteten.
• Automatiserade projektbyggen: Starta och övervaka Lean-projektbyggen som en del av automatiserade arbetsflöden eller agentstyrda kodgranskningar.

Så här sätter du upp det

Windsurf

1. Säkerställ att uv är installerat.
2. Bygg ditt Lean-projekt genom att köra lake build i projektroten.
3. Lokalisera Windsurf-konfigurationsfilen.
4. Lägg till Lean LSP MCP-servern med följande JSON-snutt:

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

5. Spara och starta om Windsurf, kontrollera sedan att MCP-servern körs.

Claude

1. Installera uv och kör lake build i ditt Lean-projekt.
2. Öppna Claudes konfigurationsfil.
3. Lägg in MCP-serverkonfigurationen:

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

4. Spara och starta om Claude, bekräfta sedan att servern är tillgänglig.

Cursor

1. Installera uv och kör lake build.
2. Öppna Cursors konfigurationsfil.
3. Lägg till Lean LSP MCP-servern:

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

4. Spara ändringarna och starta om Cursor.

Cline

1. Se till att uv är installerat och kör lake build.
2. Hitta och redigera Clines konfigurationsfil.
3. Lägg till servern:

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

4. Spara och starta om Cline.

Säkra API-nycklar

Om din installation kräver API-nycklar, använd miljövariabler för att hålla dem säkra. Exempel:

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

Så använder du denna MCP i flöden

Använda MCP i FlowHunt

För att integrera MCP-servrar i ditt FlowHunt-arbetsflöde lägger du först till MCP-komponenten i flödet och kopplar den till din AI-agent:

Klicka på MCP-komponenten för att öppna konfigurationspanelen. I systemets MCP-konfigurationssektion, infoga dina MCP-serveruppgifter med detta JSON-format:

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

När det är konfigurerat kan AI-agenten nu använda denna MCP som ett verktyg med åtkomst till alla dess funktioner och kapaciteter. Kom ihåg att ändra “lean-lsp-mcp” till det faktiska namnet på din MCP-server och byt ut URL:en mot din egen MCP-server-URL.

Översikt

Baserat på tillgänglig dokumentation och kod ger Lean LSP MCP starkt verktygsstöd för Lean-projekt men saknar explicita promptmallar eller MCP-resursdefinitioner. Sampling och roots-stöd nämns inte. Sammantaget är servern praktisk för Lean-användare men exponerar ännu inte hela spektrumet av avancerade MCP-funktioner.

MCP-poäng