Lean LSP MCP Server

Co robi serwer “Lean LSP MCP”?

Lean LSP MCP to serwer Model Context Protocol (MCP), który łączy asystentów AI z projektami Lean Theorem Prover za pomocą Language Server Protocol (LSP) wykorzystując leanclient. Umożliwia agentom i dużym modelom językowym interakcję z projektami Lean, zapewniając dostęp do diagnostyki, stanów celów, informacji o termach, dokumentacji podpowiedzi i innych funkcji. Ta integracja usprawnia workflow deweloperów Lean poprzez udostępnienie bogatego zestawu narzędzi dla agentów, w tym wyszukiwania twierdzeń, uzupełniania kodu i budowania projektów. Serwer ma na celu poprawę doświadczenia deweloperów, badaczy i agentów AI pracujących z Lean, czyniąc narzędzia Lean łatwo dostępnymi w zautomatyzowanych i interaktywnych kontekstach.

Lista promptów

Nie znaleziono informacji o szablonach promptów w repozytorium.

Lista zasobów

Nie znaleziono informacji o udostępnionych zasobach MCP w repozytorium.

Lista narzędzi

• Lean Theorem Search: Pozwala agentom wyszukiwać twierdzenia dzięki integracji z leansearch.net.
• Uzupełnianie kodu: Dostarcza podpowiedzi uzupełniania kodu dla plików Lean.
• Budowanie projektu: Umożliwia budowanie projektów za pomocą systemu build Lean.
• Diagnostyka: Zapewnia dostęp do diagnostyki projektów Lean.
• Stany celów i informacje o termach: Udostępnia informacje o stanie celu i termach dla głębszej analizy projektu.
• Dokumentacja podpowiedzi: Zwraca dokumentację po najechaniu kursorem na elementy kodu Lean.

Przykłady zastosowania tego serwera MCP

• Diagnostyka projektów Lean: Natychmiastowy dostęp do diagnostyki poprawności kodu i debugowania w ramach projektów Lean.
• Eksploracja stanów celów: Pobieranie i wyświetlanie aktualnych stanów celów na potrzeby rozwoju dowodu i planowania strategii.
• Wyszukiwanie twierdzeń: Wyszukiwanie odpowiednich twierdzeń z leansearch.net, aby pomagać w konstrukcji dowodów.
• Uzupełnianie kodu dla Lean: Inteligentne podpowiedzi i uzupełnianie kodu dla Lean, zwiększające produktywność.
• Automatyczne budowanie projektów: Uruchamianie i monitorowanie budowania projektów Lean jako część zautomatyzowanych workflow lub agentowej recenzji kodu.

Jak skonfigurować

Windsurf

1. Upewnij się, że uv jest zainstalowany.
2. Zbuduj swój projekt Lean uruchamiając lake build w katalogu głównym projektu.
3. Znajdź plik konfiguracyjny Windsurf.
4. Dodaj serwer Lean LSP MCP za pomocą poniższego fragmentu JSON:

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

5. Zapisz i zrestartuj Windsurf, a następnie sprawdź, czy serwer MCP działa.

Claude

1. Zainstaluj uv i uruchom lake build w swoim projekcie Lean.
2. Otwórz plik konfiguracyjny Claude’a.
3. Wstaw konfigurację serwera MCP:

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

4. Zapisz i zrestartuj Claude, a następnie potwierdź dostępność serwera.

Cursor

1. Zainstaluj uv i uruchom lake build.
2. Otwórz plik konfiguracyjny Cursor.
3. Dodaj serwer Lean LSP MCP:

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

4. Zapisz zmiany i zrestartuj Cursor.

Cline

1. Upewnij się, że uv jest zainstalowany i uruchom lake build.
2. Znajdź i edytuj plik konfiguracyjny Cline.
3. Dodaj serwer:

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

4. Zapisz i zrestartuj Cline.

Zabezpieczanie kluczy API

Jeśli Twoja konfiguracja wymaga kluczy API, używaj zmiennych środowiskowych, aby zachować ich bezpieczeństwo. Przykład:

{
  "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 używać tego MCP w flow

Użycie MCP w FlowHunt

Aby zintegrować serwery MCP z workflow FlowHunt, rozpocznij od dodania komponentu MCP do swojego flow i połączenia go z agentem AI:

Kliknij na komponent MCP, aby otworzyć panel konfiguracji. W sekcji konfiguracji systemu MCP wstaw szczegóły serwera MCP w tym formacie JSON:

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

Po skonfigurowaniu agent AI może korzystać z MCP jako narzędzia ze wszystkimi jego funkcjami i możliwościami. Pamiętaj, aby zmienić “lean-lsp-mcp” na faktyczną nazwę swojego serwera MCP i podać własny adres URL serwera MCP.

Przegląd

Na podstawie dostępnej dokumentacji i kodu, Lean LSP MCP zapewnia rozbudowane wsparcie narzędziowe dla projektów Lean, ale brakuje mu jawnych szablonów promptów i definicji zasobów MCP. Sampling i wsparcie dla roots nie są wspomniane. Ogólnie serwer jest praktyczny dla użytkowników Lean, choć nie udostępnia jeszcze pełnego spektrum zaawansowanych funkcji MCP.

Ocena MCP