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: v0.4.1...v0.6.0

What's Changed

• Help agents to identify incorrect input parameters in #12
• Return relevant diagnostic messages with hover information

Full Changelog: 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 #6

Full Changelog: 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: v0.3.0...v0.3.1

Features

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

Full Changelog: 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: v0.1.11...v0.2.0