oOo0oOo/lean-lsp-mcp

📋 What's Changed

• pipe setup subprocess stdio to fix #181 by @oOo0oOo in https://github.com/oOo0oOo/lean-lsp-mcp/pull/182
• docs: add tool_timeout_sec to Mistral Vibe setup by @mertunsall in https://github.com/oOo0oOo/lean-lsp-mcp/pull/184
• fix: use chunked read in lean_build to avoid buffer overflow on long lines by @mertunsall in https://github.com/oOo0oOo/lean-lsp-mcp/pull/183
• Move tool list from README to docs/tools.md and add reference link by @Sfgangloff in https://github.com/oOo0oOo/lean-lsp-mcp/pull/188
• Optional structured output for lean_goal by @Sfgangloff in https://github.com/oOo0oOo/lean-lsp-mcp/pull/189
• feat(code_actions): fall back to full-line range when no actions found by @maorbenshahar in https://github.com/oOo0oOo/lean-lsp-mcp/pull/197
• fix(multi_attempt): surface diagnostics introduced at distant lines by @maorbenshahar in https://github.com/oOo0oOo/lean-lsp-mcp/pull/198
• feat(server): add lean_minimal_hypotheses tool by @Sfgangloff in https://github.com/oOo0oOo/lean-lsp-mcp/pull/190
• + 13 more

✨ New Contributors

• @mertunsall made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/184
• @Sfgangloff made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/188
• @srghma made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/199
• Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.26.0...v0.27.0

📋 What's Changed

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

✨ New Contributors

• @jasonrute made their first contribution in https://github.com/oOo0oOo/lean-lsp-mcp/pull/174
• Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/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
• + 4 more

✨ 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
• + 1 more

✨ 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](https://arxiv.org/abs/2510.15940) 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

✨ Features

• Support `sse` and `streamable-http` transport methods
• Support bearer token authentication for `sse` and `streamable-http`
• Better instructions for `lean_multi_attempt` tool
• Expose `lake clean` in `lean_build` tool
• Full Changelog: https://github.com/oOo0oOo/lean-lsp-mcp/compare/v0.4.1...v0.6.0

📋 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

📋 Changes

• 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.