Lean LSP MCP Server

Čo robí server “Lean LSP MCP”?

Lean LSP MCP je server Model Context Protocol (MCP), ktorý prepája AI asistentov s projektmi Lean Theorem Prover cez Language Server Protocol (LSP) pomocou leanclient. Umožňuje agentom a veľkým jazykovým modelom (LLM) interagovať s Lean projektmi a poskytuje prístup k diagnostike, stavom cieľov, informáciám o termínoch, dokumentácii pri nabehnutí myšou a ďalším funkciám. Táto integrácia zjednodušuje vývojové workflow pre Lean používateľov tým, že sprístupňuje bohatú škálu agentovo orientovaných nástrojov, vrátane vyhľadávania teorém, dopĺňania kódu a funkcionality zostavovania projektov. Server je navrhnutý na zlepšenie skúsenosti vývojárov, výskumníkov a AI agentov pracujúcich s Lean tým, že Lean nástroje sprístupňuje v automatizovaných aj interaktívnych kontextoch.

Zoznam promptov

V repozitári sa nenašli žiadne informácie o šablónach promptov.

Zoznam zdrojov

V repozitári sa nenašli žiadne informácie o vystavených MCP zdrojoch.

Zoznam nástrojov

• Lean vyhľadávanie teorém: Umožňuje agentom vyhľadávať teorémy pomocou integrácie leansearch.net.
• Dopĺňanie kódu: Poskytuje návrhy na doplnenie kódu pre Lean súbory.
• Zostavenie projektu: Uľahčuje zostavovanie projektov cez Lean build systém.
• Diagnostika: Ponúka prístup k diagnostike v rámci Lean projektov.
• Stavy cieľov & informácie o termínoch: Sprístupňuje stav cieľov a informácie o termínoch pre hlbšiu analýzu projektu.
• Hover dokumentácia: Vracia dokumentáciu pri nabehnutí myšou nad prvkami Lean kódu.

Prípady použitia tohto MCP servera

• Diagnostika Lean projektov: Okamžitý prístup a zobrazenie diagnostiky pre kontrolu správnosti kódu a ladenie v Lean projektoch.
• Skúmanie stavov cieľov: Získavanie a zobrazovanie aktuálnych stavov cieľov pri vývoji dôkazov a plánovaní stratégií.
• Vyhľadávanie teorém: Vyhľadávanie relevantných teorém z leansearch.net na pomoc pri tvorbe dôkazov.
• Dopĺňanie kódu pre Lean: Inteligentné dopĺňanie kódu a návrhy pre Lean, čo zvyšuje produktivitu.
• Automatizované zostavovanie projektov: Spúšťanie a monitorovanie zostavovania Lean projektov ako súčasť automatizovaných workflow alebo agentnej kontroly kódu.

Ako to nastaviť

Windsurf

1. Uistite sa, že máte nainštalovaný uv.
2. Zostavte svoj Lean projekt spustením lake build v koreňovom adresári projektu.
3. Nájdite konfiguračný súbor Windsurf.
4. Pridajte Lean LSP MCP server pomocou nasledujúceho JSON útržku:

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

5. Uložte a reštartujte Windsurf, potom overte, že MCP server beží.

Claude

1. Nainštalujte uv a spustite lake build vo svojom Lean projekte.
2. Otvorte konfiguračný súbor Claude.
3. Vložte konfiguráciu MCP servera:

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

4. Uložte a reštartujte Claude, potom potvrďte dostupnosť servera.

Cursor

1. Nainštalujte uv a spustite lake build.
2. Otvorte konfiguračný súbor Cursor.
3. Pridajte Lean LSP MCP server:

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

4. Uložte zmeny a reštartujte Cursor.

Cline

1. Uistite sa, že uv je nainštalovaný, a spustite lake build.
2. Nájdite a upravte konfiguračný súbor Cline.
3. Pridajte server:

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

4. Uložte a reštartujte Cline.

Zabezpečenie API kľúčov

Ak vaša konfigurácia vyžaduje API kľúče, používajte environmentálne premenné na ich bezpečné uloženie. Príklad:

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

Ako používať tento MCP v tokoch

Použitie MCP vo FlowHunt

Na integráciu MCP serverov do vášho FlowHunt workflow začnite pridaním MCP komponentu do toku a jeho prepojením s vaším AI agentom:

Kliknite na MCP komponent pre otvorenie konfiguračného panelu. V sekcii systémovej MCP konfigurácie vložte údaje o vašom MCP serveri v tomto JSON formáte:

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

Po nakonfigurovaní je AI agent schopný používať tento MCP ako nástroj so všetkými jeho funkciami a možnosťami. Nezabudnite zmeniť “lean-lsp-mcp” na skutočný názov vášho MCP servera a URL nahradiť vašou vlastnou MCP adresou.

Prehľad

Na základe dostupnej dokumentácie a kódu poskytuje Lean LSP MCP silnú podporu nástrojov pre Lean projekty, ale chýbajú explicitné šablóny promptov alebo definície MCP zdrojov. Sampling a podpora roots nie sú spomenuté. Celkovo je server praktický pre Lean používateľov, no zatiaľ nevystavuje celý rozsah pokročilých MCP funkcionalít.

MCP skóre