lean-lsp-mcp

What's Changed

• Help agents to identify incorrect input parameters in https://github.com/oOo0oOo/lean-lsp-mcp/pull/12
• Return relevant diagnostic messages with hover information

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.4.0...v0.4.1

What's Changed

• LeanHammer premise search tool
• Better error responses
• Fix: Sorting lean_completions tool results, better partial results

New Contributors

• @gaearon made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/6

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.3.1...v0.4.0

Features

• Support self-hosted Lean State Search
• Improved instructions (MCP and tool): Make more concise to save tokens
• Bump dependencies
• Fix: Lean build tool

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.3.0...v0.3.1

Features

• Loogle tool
• Lean State Search tool
• Rate limiting external search tools
• Cleaner logging

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.2.0...v0.3.0

Features:

• New tool lean_run_code: Run/compile independent code snippets/files and receive diagnostic messages.
• Configuration of env variable LEAN_PROJECT_PATH no longer required.

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.1.11...v0.2.0