Lean LSP MCP-server

Hva gjør “Lean LSP MCP”-serveren?

Lean LSP MCP er en Model Context Protocol (MCP)-server som kobler AI-assistenter til Lean Theorem Prover-prosjekter via Language Server Protocol (LSP) ved bruk av leanclient. Den gjør det mulig for agenter og LLM-er å samhandle med Lean-prosjekter, og gir tilgang til diagnostikk, måltilstander, terminformasjon, hover-dokumentasjon og mer. Denne integrasjonen effektiviserer utviklingsarbeidsflyter for Lean-brukere ved å eksponere et rikt agentfokusert verktøysett, inkludert teoremsøk, kodefullføring og prosjektbyggingsfunksjonalitet. Serveren har som mål å forbedre opplevelsen for utviklere, forskere og AI-agenter som jobber med Lean, ved å gjøre Leans verktøy tilgjengelige i automatiserte og interaktive sammenhenger.

Liste over prompt-maler

Det ble ikke funnet informasjon om prompt-maler i depotet.

Liste over ressurser

Det ble ikke funnet informasjon om eksponerte MCP-ressurser i depotet.

Liste over verktøy

• Lean teoremsøk: Lar agenter søke etter teoremer via integrasjon med leansearch.net.
• Kodefullføring: Gir forslag til kodefullføring for Lean-filer.
• Prosjektbygging: Legger til rette for prosjektbygg via Leans byggesystem.
• Diagnostikk: Tilbyr tilgang til diagnostikk i Lean-prosjekter.
• Måltilstander & terminformasjon: Eksponerer måltilstand og terminformasjon for dypere prosjektanalyse.
• Hover-dokumentasjon: Returnerer dokumentasjon når man holder musepekeren over elementer i Lean-kode.

Bruksområder for denne MCP-serveren

• Prosjektdiagnostikk for Lean: Få umiddelbar tilgang til og vis diagnostikk for kodekorrigering og feilsøking i Lean-prosjekter.
• Utforsking av måltilstand: Hent og vis nåværende måltilstand for bevisutvikling og strategiplanlegging.
• Teoremsøk: Søk etter relevante teoremer fra leansearch.net for å hjelpe med bevisbygging.
• Kodefullføring for Lean: Tilby intelligent kodefullføring og forslag for Lean som øker produktiviteten.
• Automatiserte prosjektbygg: Start og overvåk Lean-prosjektbygg som del av automatiserte arbeidsflyter eller agentbasert kodegjennomgang.

Slik setter du det opp

Windsurf

1. Sørg for at uv er installert.
2. Bygg Lean-prosjektet ditt ved å kjøre lake build i prosjektroten.
3. Finn Windsurf-konfigurasjonsfilen.
4. Legg til Lean LSP MCP-serveren ved å bruke følgende JSON-snutt:

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

5. Lagre og start Windsurf på nytt, og verifiser at MCP-serveren kjører.

Claude

1. Installer uv og kjør lake build i Lean-prosjektet ditt.
2. Åpne Claudes konfigurasjonsfil.
3. Sett inn MCP-serverkonfigurasjonen:

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

4. Lagre og start Claude på nytt, og bekreft at serveren er tilgjengelig.

Cursor

1. Installer uv og kjør lake build.
2. Åpne Cursors konfigurasjonsfil.
3. Legg til Lean LSP MCP-serveren:

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

4. Lagre endringer og start Cursor på nytt.

Cline

1. Sørg for at uv er installert og kjør lake build.
2. Finn og rediger Clines konfigurasjonsfil.
3. Legg til serveren:

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

4. Lagre og start Cline på nytt.

Sikring av API-nøkler

Dersom oppsettet ditt krever API-nøkler, bruk miljøvariabler for å 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}"
      }
    }
  }
}

Slik bruker du denne MCP-en i arbeidsflyter

Bruke MCP i FlowHunt

For å integrere MCP-servere i FlowHunt-arbeidsflyten din, start med å legge til MCP-komponenten i flyten og koble den til din AI-agent:

Klikk på MCP-komponenten for å åpne konfigurasjonspanelet. I system-MCP-konfigurasjonsseksjonen setter du inn MCP-serverdetaljene dine med dette JSON-formatet:

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

Når dette er konfigurert, kan AI-agenten nå bruke denne MCP-en som et verktøy med tilgang til alle dens funksjoner og muligheter. Husk å endre “lean-lsp-mcp” til det faktiske navnet på din MCP-server og bytt ut URL-en med din egen MCP-server-URL.

Oversikt

Basert på tilgjengelig dokumentasjon og kode gir Lean LSP MCP sterk verktøystøtte for Lean-prosjekter, men mangler eksplisitte prompt-maler eller MCP-ressursdefinisjoner. Sampling og roots-støtte er ikke nevnt. Alt i alt er serveren praktisk for Lean-brukere, men eksponerer foreløpig ikke hele spekteret av avanserte MCP-funksjoner.

MCP-score