lean-lsp-mcp

• Fixed REPL memory limits
• Single scratch pool
• Simplified local loogle
• Bump dependencies

Full Changelog: v0.28.0...v0.29.0

Migrates the MCP server onto the async leanclient stack, improves slow-file/prewarm behavior, supports Lean 4.30 diagnostics and completions, fixes key correctness edge cases, and bumps dependencies.

Full Changelog: v0.27.0...v0.28.0

What's Changed

• pipe setup subprocess stdio to fix #181 by @oOo0oOo in #182
• docs: add tool_timeout_sec to Mistral Vibe setup by @mertunsall in #184
• fix: use chunked read in lean_build to avoid buffer overflow on long lines by @mertunsall in #183
• Move tool list from README to docs/tools.md and add reference link by @Sfgangloff in #188
• Optional structured output for lean_goal by @Sfgangloff in #189
• feat(code_actions): fall back to full-line range when no actions found by @maorbenshahar in #197
• fix(multi_attempt): surface diagnostics introduced at distant lines by @maorbenshahar in #198
• feat(server): add lean_minimal_hypotheses tool by @Sfgangloff in #190
• Make lean_build cache fetch opt-in by @mertunsall in #200
• Updates the lean_leanfinder tool served by the Hugging Face endpoint by @mikeljl in #194
• doc(tunnel) Document Secure MCP Tunnel setup by @eliasjudin in #195
• docs: add guide for adding a new MCP tool by @Sfgangloff in #191
• Bump test project to Lean v4.30.0 by @oOo0oOo in #202
• Add flake.nix by @srghma in #199
• Fix severity schema for Gemini/Vertex function calling (#185) by @oOo0oOo in #203
• Skip rate limits for self-hosted search backends; raise LeanSearch limit by @oOo0oOo in #204
• Fix local loogle: search-path clobber and CLI flag drift (#193) by @oOo0oOo in #205
• Refactor: config module + split server.py into a tools/ subpackage by @oOo0oOo in #206
• Make the server type-check clean under ty + add ty to CI by @oOo0oOo in #207
• Bump dependencies (leanclient 0.11.0, mcp 1.27.2, lockfile) by @oOo0oOo in #208
• Fix release blockers: wheel packaging (tools/) + minimal_hypotheses no-binder case by @oOo0oOo in #209

New Contributors

• @mertunsall made their first contribution in #184
• @Sfgangloff made their first contribution in #188
• @srghma made their first contribution in #199

Full Changelog: v0.26.0...v0.27.0

Full Changelog: v0.25.0...v0.26.0

What's Changed

• Update the README to support Mistral Vibe by @jasonrute in #174
• feat: add --version / -v flag to CLI by @oOo0oOo in #178
• Fallback to elan lean path for stdlib search by @oOo0oOo in #179
• timed_out field and max_open_files variable by @maorbenshahar in #163
• Harden path policy and remote project binding by @eliasjudin in #175
• shared client by @maorbenshahar in #166

New Contributors

• @jasonrute made their first contribution in #174

Full Changelog: v0.25.0...v0.26.0

What's Changed

• Fix/orphaned profile processes by @maorbenshahar in https://github.com/oOo0oOo/lean-lsp-mcp/pull/165
• Fix/multi attempt context and column by @jeffrey-dot-li in https://github.com/oOo0oOo/lean-lsp-mcp/pull/171
• feat: add lean_references tool by @Arrow7000 in https://github.com/oOo0oOo/lean-lsp-mcp/pull/168

New Contributors

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

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.24.0...v0.25.0

What's Changed

• Add configurable build concurrency modes by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/124
• Add strict project-root mode and runtime tool controls by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/138
• Add secure container packaging defaults by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/143
• Feat/diagnostic severity filter by @jeffrey-dot-li in https://github.com/oOo0oOo/lean-lsp-mcp/pull/161
• fix: fix the path problem by @pelicanhere in https://github.com/oOo0oOo/lean-lsp-mcp/pull/167

New Contributors

• @jeffrey-dot-li made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/161
• @pelicanhere made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/167

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.23.1...v0.24.0

What's Changed

• Fix stdio transport instability without stdout fd mutation by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/148
• fix: share loogle subprocess across HTTP sessions by @spitters in https://github.com/oOo0oOo/lean-lsp-mcp/pull/145
• Chore/various chores by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/149
• Fix parse_axioms failing on multiline #print axioms output by @maorbenshahar in https://github.com/oOo0oOo/lean-lsp-mcp/pull/152
• Harden teardown to prevent transport drops by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/150
• feat: allow passing Lean dir path via CLI by @zeyu-zheng in https://github.com/oOo0oOo/lean-lsp-mcp/pull/151
• Harden loogle init and teardown error handling by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/154
• Rewrite lean_verify to use append-and-restore instead of olean files by @maorbenshahar in https://github.com/oOo0oOo/lean-lsp-mcp/pull/155
• [fix] Windows compatibility: encoding, path separators, nested projects by @elazarg in https://github.com/oOo0oOo/lean-lsp-mcp/pull/156
• [fix] Include file path in error messages for failed path resolution by @elazarg in https://github.com/oOo0oOo/lean-lsp-mcp/pull/158
• feat: Make Loogle remote URL configurable via LOOGLE_URL by @dirkenglund in https://github.com/oOo0oOo/lean-lsp-mcp/pull/153
• local_search includes namespace

New Contributors

• @spitters made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/145
• @maorbenshahar made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/152
• @zeyu-zheng made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/151
• @elazarg made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/156
• @dirkenglund made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/153

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.22.0...v0.23.1

What's Changed

• Fix multi_attempt state leak via forced reopen by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/136
• New tool: Code actions by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/146
• New tool: Verify by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/147

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.21.0...v0.22.0

What's Changed

• Improve local loogle install diagnostics by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/123
• Handle Ctrl+C cleanly by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/128
• Improve lean_local_search relevance ordering by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/135
• Feature/widget support by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/144

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.20.0...v0.21.0

What's Changed

• Use REPL for lean_multi_attempt by @alok & @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/120
• Issue/117 by @dcolazin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/119

New Contributors

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

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.19.0...v0.20.0

What's Changed

• Feature/profiling tool by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/114

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.18.0...v0.19.0

What's Changed

• ci: Add scheduled/manual workflow for integration tests by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/91
• ci: Commit test_project (was gitignored) by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/111
• perf: make network tools non-blocking by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/75
• feat: Add structured diagnostics with success and failed_dependencies by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/101
• Add pytest-timeout to dev dependencies by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/112

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.17.0...v0.18.0

What's Changed

• perf: early-exit ripgrep search by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/74
• fix: Return structured objects from list-returning tools by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/81
• Add CI workflow for linting and testing by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/87
• Fix silent failures in MCP tools by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/85
• Add project-specific library indexing for local loogle by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/80
• feat: Return structured goal lists from lean_goal tool by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/89
• Various speedups from leanclient 0.7.0

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.16.0...v0.17.0

Breaking Changes

Tool responses are now structured differently. This is a breaking change! Agents should handle this just fine but custom agents might require changes.

What's Changed

• Add local loogle support to bypass rate limits by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/68
• Add MCP ToolAnnotations and structured output for all tools by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/69
• Fix silent loogle failures from stale toolchain cache by @alok in https://github.com/oOo0oOo/lean-lsp-mcp/pull/71

New Contributors

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

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.14.1...v0.16.0

What's Changed

• [feature] Support explicit project root for local search by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/65
• [feature] New tool: lean_file_outline by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/66

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.13.0...v0.14.1

What's Changed

• Add declaration_name parameter to lean_diagnostic_messages by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/60
• Add line range parameter to lean_diagnostic_messages

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.12.0...v0.13.0

What's Changed

• Diagnostics can be limited by line range to prevent waiting for full file to process.
• Speedup: Update files instead of closing and reopening.
• Handle doc-less loogle hits without errors by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/46
• Update README with WSL2 VSCode instructions by @dlebedinsky in https://github.com/oOo0oOo/lean-lsp-mcp/pull/40
• Ensure multi_attempt cleans up Lean files and align rate limits by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/47
• Ensure project activation uses Path objects by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/48
• Avoid mutating snippets in lean_multi_attempt by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/50
• update Lean Finder endpoint + response parsing + tool description by @mikeljl in https://github.com/oOo0oOo/lean-lsp-mcp/pull/52
• Restrict get_relative_file_path to project root by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/54

New Contributors

• @dlebedinsky made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/40
• @mikeljl made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/52

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.11.0...v0.12.0

What's Changed

• New Tool: Semantic search using Lean Finder by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/45
• Show build progress by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/37
• Harden run_code temporary snippet cleanup by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/41
• Serialise client startup; fix UTF‑16 ranges and build reset by @eliasjudin in https://github.com/oOo0oOo/lean-lsp-mcp/pull/43
• Chore/bump leanclient 0.4.0: Automatically build dependencies when stale by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/44

New Contributors

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

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.10.0...v0.11.0

What's Changed

• Significant speedups thanks to improved handling of blocking and building in leanclient.
• Various other improvements such as better cleanup and logging in leanclient.
• Add orjson>=3.11.1 for Python 3.14 compatibility by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/31

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.9.0...v0.10.0

What's Changed

• Local search tool to reduce API hallucinations by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/29
• Feature/automated tests by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/28

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.8.0...v0.9.0

What's Changed

• Add diagnostic logging to update_file for #21 by @jessealama in https://github.com/oOo0oOo/lean-lsp-mcp/pull/26
• Set logging verbosity using env variable LEAN_LOG_LEVEL
• Bump dependencies

New Contributors

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

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.7.0...v0.8.0

What's Changed

• feat: Add host and port arguments for transport by @lenianiva in https://github.com/oOo0oOo/lean-lsp-mcp/pull/23
• Improved instructions
• Remove environment variables from MCP config
• Bump dependencies

New Contributors

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

Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.6.0...v0.7.0