Skip to content

Releases: Lemmy00/LeanProbe

LeanProbe 0.2.2

13 May 21:44

Choose a tag to compare

What's Changed

  • Added lean_probe_capabilities MCP tool for reporting LeanProbe readiness, project-root detection, selected REPL path, and live session state.
  • Added lean-probe capabilities CLI command with matching readiness output.
  • Documented how LeanProbe complements LSP-backed Lean MCP tools such as lean-lsp-mcp.
  • Updated tests for the new MCP and CLI capability surfaces.

Validation

  • python -m pytest -q
  • python -m ruff check .
  • python -m build
  • python -m twine check dist/*

LeanProbe 0.2.1

13 May 20:15

Choose a tag to compare

Patch release for LeanProbe MCP setup docs.

  • Documents that stdio MCP clients should keep LEAN_PROBE_AUTO_BUILD=0.
  • Explains that Lean/Lake projects should be built before starting LeanProbe MCP.
  • Prevents MCP transport corruption from build output written to stdout.

Install:

python -m pip install -U lean-probe

MCP:

python -m pip install -U "lean-probe[mcp]"
lean-probe mcp

LeanProbe 0.2.0

13 May 19:26

Choose a tag to compare

First public LeanProbe release.

Install:

python -m pip install lean-probe

MCP support:

python -m pip install "lean-probe[mcp]"
lean-probe mcp

Highlights:

  • Standalone Python package, CLI, and MCP server for LeanInteract-backed Lean feedback.
  • Cached same-file declaration checks.
  • Diagnostics, tactic metadata, proof-state stepping, and feedback_lean.
  • Benchmarks for repeated target checks and sequential same-file checks.
  • Python 3.10-3.13 support across Linux, macOS, and Windows.