Lean LSP MCP Server

Hvad gør “Lean LSP MCP”-serveren?

Lean LSP MCP er en Model Context Protocol (MCP)-server, der forbinder AI-assistenter med Lean Theorem Prover-projekter via Language Server Protocol (LSP) ved hjælp af leanclient. Den gør det muligt for agenter og LLM’er at interagere med Lean-projekter og giver adgang til diagnostik, målangivelser, terminformation, hover-dokumentation og meget mere. Denne integration effektiviserer arbejdsflowet for Lean-brugere ved at eksponere et rigt agentfokuseret værktøjssæt, herunder sætningesøgning, kodefuldførelse og projekt-build-funktionalitet. Serveren har til formål at forbedre oplevelsen for udviklere, forskere og AI-agenter, der arbejder med Lean, ved at gøre Leans værktøjer tilgængelige i automatiserede og interaktive sammenhænge.

Liste over prompts

Der blev ikke fundet information om prompt-skabeloner i repositoryet.

Liste over ressourcer

Der blev ikke fundet information om eksponerede MCP-ressourcer i repositoryet.

Liste over værktøjer

• Lean sætningesøgning: Giver agenter mulighed for at søge efter sætninger via leansearch.net-integration.
• Kodefuldførelse: Giver kodeforslag til Lean-filer.
• Projekt-build: Muliggør projekt-builds via Leans build-system.
• Diagnostik: Giver adgang til diagnostik i Lean-projekter.
• Målangivelser & terminformation: Eksponerer målangivelser og terminformation til dybere projektdiagnose.
• Hover-dokumentation: Returnerer dokumentation ved mouse-over af Lean-kodeelementer.

Anvendelsestilfælde for denne MCP-server

• Lean-projektdiagnostik: Få øjeblikkelig adgang til og visning af diagnostik for kodekorrekthed og fejlfinding i Lean-projekter.
• Målangivelses-udforskning: Hent og vis aktuelle målangivelser til bevisudvikling og strategiplanlægning.
• Sætningesøgning: Søg efter relevante sætninger fra leansearch.net til brug i beviskonstruktion.
• Kodefuldførelse for Lean: Tilbyd intelligente kodeforslag og fuldførelser for Lean og øg produktiviteten.
• Automatiserede projekt-builds: Udløs og overvåg Lean-projekt-builds som del af automatiserede workflows eller agent-baseret kodegennemgang.

Sådan sættes den op

Windsurf

1. Sørg for at uv er installeret.
2. Byg dit Lean-projekt ved at køre lake build i projektets rodmappe.
3. Find Windsurf-konfigurationsfilen.
4. Tilføj Lean LSP MCP-serveren ved at indsætte følgende JSON-snippet:

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

5. Gem og genstart Windsurf, og verificér at MCP-serveren kører.

Claude

1. Installer uv og kør lake build i dit Lean-projekt.
2. Åbn Claudes konfigurationsfil.
3. Indsæt MCP-serverkonfigurationen:

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

4. Gem og genstart Claude, og bekræft at serveren er tilgængelig.

Cursor

1. Installer uv og kør lake build.
2. Åbn Cursors konfigurationsfil.
3. Tilføj Lean LSP MCP-serveren:

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

4. Gem ændringer og genstart Cursor.

Cline

1. Sikr dig at uv er installeret og kør lake build.
2. Find og redigér Clines konfigurationsfil.
3. Tilføj serveren:

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

4. Gem og genstart Cline.

Sikring af API-nøgler

Hvis din opsætning kræver API-nøgler, skal du bruge miljøvariabler for at holde dem sikre. Eksempel:

{
  "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ådan bruges denne MCP i flows

Brug af MCP i FlowHunt

For at integrere MCP-servere i dit FlowHunt-arbejdsflow skal du starte med at tilføje MCP-komponenten til dit flow og forbinde den til din AI-agent:

Klik på MCP-komponenten for at åbne konfigurationspanelet. Indsæt dine MCP-serverdetaljer i systemets MCP-konfigurationssektion ved at bruge dette JSON-format:

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

Når det er konfigureret, kan AI-agenten nu bruge denne MCP som et værktøj med adgang til alle dens funktioner og muligheder. Husk at ændre “lean-lsp-mcp” til det faktiske navn på din MCP-server og udskifte URL’en med din egen MCP-server-URL.

Oversigt

Ud fra den tilgængelige dokumentation og kode giver Lean LSP MCP stærk værktøjsunderstøttelse til Lean-projekter, men mangler eksplicitte prompt-skabeloner eller MCP-ressourcedefinitioner. Sampling og roots-understøttelse er ikke nævnt. Samlet set er serveren praktisk for Lean-brugere, men eksponerer endnu ikke hele spektret af avancerede MCP-funktioner.

MCP-score