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