Serveur Lean LSP MCP

Que fait le serveur “Lean LSP MCP” ?

Lean LSP MCP est un serveur Model Context Protocol (MCP) qui connecte les assistants IA aux projets Lean Theorem Prover via le Language Server Protocol (LSP) en utilisant leanclient. Il permet aux agents et LLMs d’interagir avec des projets Lean, donnant accès aux diagnostics, états de but, informations sur les termes, documentation contextuelle, etc. Cette intégration simplifie les workflows de développement pour les utilisateurs de Lean en exposant un riche ensemble d’outils orientés agent, dont la recherche de théorèmes, la complétion de code et la compilation de projet. Le serveur vise à améliorer l’expérience des développeurs, chercheurs et agents IA travaillant avec Lean en rendant les outils Lean accessibles dans des contextes automatisés et interactifs.

Liste des prompts

Aucune information sur des modèles de prompt n’a été trouvée dans le dépôt.

Liste des ressources

Aucune information sur des ressources MCP exposées n’a été trouvée dans le dépôt.

Liste des outils

• Recherche de théorèmes Lean : Permet aux agents de rechercher des théorèmes via l’intégration leansearch.net.
• Complétion de code : Fournit des suggestions de complétion pour les fichiers Lean.
• Compilation de projet : Facilite les builds de projets via le système de build Lean.
• Diagnostics : Offre l’accès aux diagnostics dans les projets Lean.
• États de but & Informations sur les termes : Expose les états de but et les informations de terme pour une analyse approfondie du projet.
• Documentation contextuelle : Retourne la documentation lors du survol des éléments de code Lean.

Cas d’usage de ce serveur MCP

• Diagnostics de projet Lean : Accédez instantanément et affichez les diagnostics pour la correction et le débogage au sein des projets Lean.
• Exploration des états de but : Récupérez et affichez les états de but actuels pour le développement de preuves et la planification de stratégies.
• Recherche de théorèmes : Recherchez des théorèmes pertinents via leansearch.net pour aider à la construction de preuves.
• Complétion de code pour Lean : Proposez une complétion de code intelligente et des suggestions pour Lean, améliorant ainsi la productivité.
• Builds de projet automatisés : Déclenchez et surveillez les builds Lean dans des workflows automatisés ou des revues de code par agent.

Comment le configurer

Windsurf

1. Assurez-vous que uv est installé.
2. Compilez votre projet Lean en exécutant lake build à la racine du projet.
3. Localisez le fichier de configuration Windsurf.
4. Ajoutez le serveur Lean LSP MCP avec l’extrait JSON suivant :

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

5. Sauvegardez et redémarrez Windsurf, puis vérifiez que le serveur MCP fonctionne.

Claude

1. Installez uv puis lancez lake build dans votre projet Lean.
2. Ouvrez le fichier de configuration de Claude.
3. Insérez la configuration du serveur MCP :

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

4. Sauvegardez et redémarrez Claude, puis confirmez que le serveur est disponible.

Cursor

1. Installez uv et lancez lake build.
2. Ouvrez le fichier de configuration de Cursor.
3. Ajoutez le serveur Lean LSP MCP :

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

4. Sauvegardez les modifications et redémarrez Cursor.

Cline

1. Vérifiez que uv est installé et lancez lake build.
2. Trouvez puis éditez le fichier de configuration Cline.
3. Ajoutez le serveur :

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

4. Sauvegardez et redémarrez Cline.

Sécuriser les clés API

Si votre configuration nécessite des clés API, utilisez des variables d’environnement pour les sécuriser. Exemple :

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

Comment utiliser ce MCP dans vos flows

Utilisation de MCP dans FlowHunt

Pour intégrer des serveurs MCP dans votre workflow FlowHunt, commencez par ajouter le composant MCP à votre flow et connectez-le à votre agent IA :

Cliquez sur le composant MCP pour ouvrir le panneau de configuration. Dans la section de configuration système MCP, insérez les détails de votre serveur MCP en utilisant ce format JSON :

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

Une fois configuré, l’agent IA pourra utiliser ce MCP comme outil avec accès à toutes ses fonctions et capacités. Pensez à remplacer “lean-lsp-mcp” par le nom réel de votre serveur MCP et à renseigner l’URL de votre propre serveur MCP.

Aperçu

D’après la documentation et le code disponibles, Lean LSP MCP propose un support d’outillage solide pour les projets Lean mais n’inclut pas de modèles de prompt explicites ni de définitions de ressources MCP. Le sampling et le support des racines ne sont pas mentionnés. Globalement, ce serveur est pratique pour les utilisateurs Lean mais n’expose pas encore toutes les fonctionnalités avancées MCP.

Score MCP