Lean LSP MCP Server

Co dělá server “Lean LSP MCP”?

Lean LSP MCP je server Model Context Protocolu (MCP), který propojuje AI asistenty s projekty Lean Theorem Prover prostřednictvím Language Server Protocolu (LSP) pomocí leanclientu. Umožňuje agentům a LLM interagovat s Lean projekty a poskytuje přístup k diagnostice, stavům cílů, informacím o termínech, dokumentaci při najetí myší a dalším funkcím. Tato integrace zjednodušuje pracovní postupy vývoje pro uživatele Lean tím, že poskytuje bohatou sadu nástrojů zaměřených na agenty, včetně vyhledávání vět, doplňování kódu a funkcionality sestavení projektu. Server si klade za cíl zlepšit zkušenosti vývojářů, výzkumníků i AI agentů pracujících s Lean tím, že zpřístupňuje nástroje Lean v automatizovaných i interaktivních kontextech.

Seznam promptů

V repozitáři nebyly nalezeny žádné informace o šablonách promptů.

Připraveni rozšířit své podnikání?

Začněte svou bezplatnou zkušební verzi ještě dnes a viďte výsledky během několika dní.

Požádat o demo Přihlásit se

Seznam zdrojů

V repozitáři nebyly nalezeny žádné informace o vystavených MCP zdrojích.

Seznam nástrojů

• Lean Theorem Search: Umožňuje agentům vyhledávat věty pomocí integrace leansearch.net.
• Doplňování kódu: Nabízí návrhy na doplnění kódu pro Lean soubory.
• Sestavení projektu: Umožňuje sestavení projektů přes Lean build systém.
• Diagnostika: Zprostředkovává přístup k diagnostice v Lean projektech.
• Stavy cílů & informace o termínech: Zpřístupňuje informace o stavech cílů a termínech pro hlubší analýzu projektu.
• Dokumentace při najetí: Vrací dokumentaci při najetí na prvky Lean kódu.

Přihlaste se k odběru newsletteru

Získejte nejnovější tipy, trendy a nabídky zdarma.

E-mailová adresa

Přihlásit se

Případy použití tohoto MCP serveru

• Diagnostika Lean projektů: Okamžitý přístup a zobrazení diagnostiky pro správnost kódu a ladění v Lean projektech.
• Zkoumání stavů cílů: Získání a zobrazení aktuálních stavů cílů při vývoji důkazů a plánování strategie.
• Vyhledávání vět: Vyhledávání relevantních vět z leansearch.net na podporu konstrukce důkazů.
• Doplňování kódu pro Lean: Poskytuje inteligentní doplňování a návrhy pro Lean, zvyšuje produktivitu.
• Automatizované sestavení projektů: Spouštění a sledování sestavení Lean projektů v rámci automatizovaných workflow nebo revize kódu agentem.

Jak jej nastavit

Windsurf

1. Ujistěte se, že máte nainstalován uv .
2. Sestavte svůj Lean projekt příkazem lake build v kořenovém adresáři projektu.
3. Najděte konfigurační soubor Windsurf.
4. Přidejte Lean LSP MCP server pomocí následujícího JSON úryvku:

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

5. Uložte a restartujte Windsurf, poté ověřte, že MCP server běží.

Claude

1. Nainstalujte uv a spusťte lake build ve svém Lean projektu.
2. Otevřete konfigurační soubor Claude.
3. Vložte konfiguraci MCP serveru:

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

4. Uložte a restartujte Claude, poté ověřte dostupnost serveru.

Cursor

1. Nainstalujte uv a spusťte lake build.
2. Otevřete konfigurační soubor Cursor.
3. Přidejte Lean LSP MCP server:

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

4. Uložte změny a restartujte Cursor.

Cline

1. Ujistěte se, že máte nainstalován uv a spusťte lake build.
2. Najděte a upravte konfigurační soubor Cline.
3. Přidejte server:

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

4. Uložte a restartujte Cline.

Zabezpečení API klíčů

Pokud vaše nastavení vyžaduje API klíče, použijte k jejich zabezpečení proměnné prostředí. Pří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}"
      }
    }
  }
}

Jak tento MCP použít uvnitř flow

Použití MCP ve FlowHunt

Pro integraci MCP serverů do svého FlowHunt workflow začněte přidáním MCP komponenty do svého flow a jejím propojením s AI agentem:

Klikněte na MCP komponentu pro otevření panelu nastavení. Do sekce systémové konfigurace MCP vložte detaily vašeho MCP serveru v tomto JSON formátu:

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

Po konfiguraci může AI agent tento MCP využívat jako nástroj se všemi jeho funkcemi a možnostmi. Nezapomeňte změnit “lean-lsp-mcp” na skutečný název vašeho MCP serveru a URL nahradit vaší vlastní adresou MCP serveru.

Přehled

Na základě dostupné dokumentace a kódu poskytuje Lean LSP MCP silnou podporu nástrojů pro Lean projekty, ale postrádá explicitní šablony promptů a definice MCP zdrojů. Podpora samplingu a roots není zmíněna. Celkově je server praktický pro Lean uživatele, ale zatím nevystavuje plné spektrum pokročilých MCP funkcí.

MCP skóre