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.

Ready to grow your business?

Start your free trial today and see results within days.

Request demo Log in

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.

Join our newsletter

Get latest tips, trends, and deals for free.

Email address

Subscribe

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