Servidor Lean LSP MCP

¿Qué hace el servidor “Lean LSP MCP”?

Lean LSP MCP es un servidor del Protocolo de Contexto de Modelo (MCP) que conecta asistentes de IA con proyectos de Lean Theorem Prover a través del Protocolo de Servidor de Lenguaje (LSP) usando leanclient. Permite a los agentes y LLMs interactuar con proyectos Lean, brindando acceso a diagnósticos, estados de meta, información de términos, documentación emergente y más. Esta integración agiliza los flujos de trabajo de desarrollo para usuarios de Lean al exponer un conjunto de herramientas rico y enfocado en agentes, incluyendo búsqueda de teoremas, autocompletado de código y funcionalidad de construcción de proyectos. El servidor busca mejorar la experiencia de desarrolladores, investigadores y agentes de IA que trabajan con Lean haciendo que las herramientas de Lean sean accesibles en contextos automatizados e interactivos.

Lista de Prompts

No se encontró información sobre plantillas de prompts en el repositorio.

Lista de Recursos

No se encontró información sobre recursos MCP expuestos en el repositorio.

Lista de Herramientas

• Búsqueda de Teoremas en Lean: Permite a los agentes buscar teoremas utilizando la integración con leansearch.net.
• Autocompletado de Código: Proporciona sugerencias de autocompletado para archivos Lean.
• Construcción de Proyectos: Facilita la construcción de proyectos mediante el sistema de construcción de Lean.
• Diagnósticos: Ofrece acceso a diagnósticos dentro de proyectos Lean.
• Estados de Meta & Información de Términos: Expone información de estado de meta y de términos para un análisis más profundo del proyecto.
• Documentación Emergente: Devuelve documentación al pasar el cursor sobre elementos de código Lean.

Casos de Uso de este Servidor MCP

• Diagnósticos de Proyectos Lean: Accede y muestra al instante diagnósticos para la corrección de código y depuración dentro de proyectos Lean.
• Exploración de Estados de Meta: Recupera y muestra estados de meta actuales para el desarrollo de pruebas y planificación de estrategias.
• Búsqueda de Teoremas: Busca teoremas relevantes desde leansearch.net para ayudar en la construcción de pruebas.
• Autocompletado de Código para Lean: Proporciona autocompletado inteligente y sugerencias para Lean, mejorando la productividad.
• Construcción Automatizada de Proyectos: Inicia y monitorea construcciones de proyectos Lean como parte de flujos de trabajo automatizados o revisiones de código por agentes.

Cómo configurarlo

Windsurf

1. Asegúrate de que uv esté instalado.
2. Construye tu proyecto Lean ejecutando lake build en la raíz de tu proyecto.
3. Localiza el archivo de configuración de Windsurf.
4. Agrega el servidor Lean LSP MCP usando el siguiente fragmento JSON:

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

5. Guarda y reinicia Windsurf, luego verifica que el servidor MCP esté en funcionamiento.

Claude

1. Instala uv y ejecuta lake build en tu proyecto Lean.
2. Abre el archivo de configuración de Claude.
3. Inserta la configuración del servidor MCP:

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

4. Guarda y reinicia Claude, luego confirma que el servidor esté disponible.

Cursor

1. Instala uv y ejecuta lake build.
2. Abre el archivo de configuración de Cursor.
3. Agrega el servidor Lean LSP MCP:

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

4. Guarda los cambios y reinicia Cursor.

Cline

1. Asegúrate de que uv esté instalado y ejecuta lake build.
2. Encuentra y edita el archivo de configuración de Cline.
3. Agrega el servidor:

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

4. Guarda y reinicia Cline.

Seguridad de las Claves API

Si tu configuración requiere claves API, usa variables de entorno para mantenerlas seguras. Ejemplo:

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

Cómo usar este MCP en flujos

Uso de MCP en FlowHunt

Para integrar servidores MCP en tu flujo de trabajo en FlowHunt, comienza agregando el componente MCP a tu flujo y conectándolo a tu agente de IA:

Haz clic en el componente MCP para abrir el panel de configuración. En la sección de configuración MCP del sistema, inserta los detalles de tu servidor MCP usando este formato JSON:

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

Una vez configurado, el agente de IA ya puede usar este MCP como una herramienta con acceso a todas sus funciones y capacidades. Recuerda cambiar “lean-lsp-mcp” por el nombre real de tu servidor MCP y reemplazar la URL con la URL de tu propio servidor MCP.

Resumen

Según la documentación y el código disponibles, Lean LSP MCP ofrece un sólido soporte de herramientas para proyectos Lean, pero carece de plantillas de prompts explícitas o definiciones de recursos MCP. No se mencionan el soporte de muestreo ni de raíces. En general, el servidor es práctico para usuarios de Lean, pero aún no expone todo el espectro de funciones avanzadas de MCP.

Puntuación MCP