Lean LSP MCP Server

O que faz o servidor “Lean LSP MCP”?

Lean LSP MCP é um servidor Model Context Protocol (MCP) que conecta assistentes de IA a projetos Lean Theorem Prover via o Language Server Protocol (LSP) usando o leanclient. Ele permite que agentes e LLMs interajam com projetos Lean, oferecendo acesso a diagnósticos, estados de meta, informações de termos, documentação ao passar o mouse e mais. Essa integração otimiza os fluxos de trabalho de desenvolvimento para usuários Lean ao expor um conjunto de ferramentas voltadas para agentes, incluindo busca de teoremas, autocompletar código e funcionalidades de build de projeto. O objetivo do servidor é aprimorar a experiência de desenvolvedores, pesquisadores e agentes de IA que trabalham com Lean, tornando as ferramentas do Lean acessíveis em contextos automatizados e interativos.

Lista de Prompts

Nenhuma informação sobre templates de prompt foi encontrada no repositório.

Lista de Recursos

Nenhuma informação sobre recursos MCP expostos foi encontrada no repositório.

Lista de Ferramentas

• Busca de Teoremas Lean: Permite que agentes busquem teoremas usando integração com leansearch.net.
• Autocompletar Código: Oferece sugestões de autocompletar para arquivos Lean.
• Build de Projeto: Facilita builds de projeto através do sistema de build do Lean.
• Diagnósticos: Oferece acesso a diagnósticos dentro de projetos Lean.
• Estados de Meta & Informações de Termos: Expõe informações de estado de meta e termos para análise mais profunda do projeto.
• Documentação ao Passar o Mouse: Retorna documentação ao passar o mouse sobre elementos do código Lean.

Casos de Uso deste Servidor MCP

• Diagnóstico de Projetos Lean: Acesse e visualize instantaneamente diagnósticos para correção e depuração de código em projetos Lean.
• Exploração de Estado de Meta: Recupere e exiba estados de meta atuais para desenvolvimento de provas e planejamento de estratégias.
• Busca de Teoremas: Busque teoremas relevantes do leansearch.net para auxiliar na construção de provas.
• Autocompletar Código para Lean: Forneça autocompletar inteligente e sugestões para Lean, aumentando a produtividade.
• Builds de Projeto Automatizados: Acione e monitore builds de projetos Lean como parte de fluxos de trabalho automatizados ou revisão de código por agentes.

Como configurar

Windsurf

1. Certifique-se de que o uv está instalado.
2. Construa seu projeto Lean executando lake build na raiz do seu projeto.
3. Localize o arquivo de configuração do Windsurf.
4. Adicione o servidor Lean LSP MCP usando o seguinte trecho JSON:

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

5. Salve e reinicie o Windsurf, depois verifique se o servidor MCP está ativo.

Claude

1. Instale o uv e execute lake build no seu projeto Lean.
2. Abra o arquivo de configuração do Claude.
3. Insira a configuração do servidor MCP:

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

4. Salve e reinicie o Claude, depois confirme que o servidor está disponível.

Cursor

1. Instale o uv e execute lake build.
2. Abra o arquivo de configuração do Cursor.
3. Adicione o servidor Lean LSP MCP:

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

4. Salve as alterações e reinicie o Cursor.

Cline

1. Certifique-se que o uv está instalado e execute lake build.
2. Localize e edite o arquivo de configuração do Cline.
3. Adicione o servidor:

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

4. Salve e reinicie o Cline.

Protegendo chaves de API

Se sua configuração exigir chaves de API, use variáveis de ambiente para mantê-las seguras. Exemplo:

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

Como usar este MCP em fluxos

Usando MCP no FlowHunt

Para integrar servidores MCP ao seu fluxo de trabalho FlowHunt, comece adicionando o componente MCP ao seu fluxo e conectando-o ao seu agente de IA:

Clique no componente MCP para abrir o painel de configuração. Na seção de configuração do sistema MCP, insira os detalhes do seu servidor MCP usando este formato JSON:

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

Uma vez configurado, o agente de IA poderá usar este MCP como ferramenta com acesso a todas as suas funções e capacidades. Lembre-se de alterar “lean-lsp-mcp” para o nome real do seu servidor MCP e substituir a URL pela URL do seu servidor MCP.

Visão Geral

Com base na documentação e código disponíveis, o Lean LSP MCP oferece forte suporte de ferramentas para projetos Lean, mas não possui templates explícitos de prompt ou definições de recursos MCP. Suporte a sampling e roots não são mencionados. No geral, o servidor é prático para usuários Lean, mas ainda não expõe todo o espectro de recursos avançados do MCP.

Pontuação MCP