lean4repo-utils

Utilities for managing Lean 4 repositories: two composite GitHub Actions and a CLI, sharing a single OpenRouter-backed LLM layer.

Tool	What it does	Use as
summary/	AI-generated summaries for Lean 4 pull requests (multi-agent pipeline: triage, per-file summaries, synthesis, optional title validation and instruction checks).	uses: alexanderlhicks/lean4repo-utils/summary@0.3
review/	AI code review for Lean 4 pull requests: spec-grounded per-file review, cross-file analysis, dependent-impact pass, adversarial finding verification, real Lean toolchain access for agents.	uses: alexanderlhicks/lean4repo-utils/review@0.3
sorry-tracker/	CLI that finds sorry/admit obligations in a Lean repo and opens detailed, LLM-analyzed GitHub issues for them.	cd sorry-tracker && uv run sorry-tracker ...
common/	Shared library leanrepo-common: the OpenRouter LLM provider (leanrepo_common.llm_provider), Lean 4 source utilities (leanrepo_common.lean_utils), and diff parsing (leanrepo_common.diff_utils).	dependency of the three tools

Evaluation status (0.3, 2026-07-25): initial ArkLib and evm-asm runs produced useful analysis, but final-output quality was inconsistent: one strong summary, one title-only/noisy summary, and one review with the correct high-level conclusion but 0/2 recall on the human-confirmed actionable findings. Treat AI prose as reviewer assistance, not a substitute for CI or human review. The maintainer's (unpublished) roadmap tracks measured follow-ups and release criteria.

All LLM access goes through OpenRouter: one API key, models selected by slug (e.g. anthropic/claude-opus-4.8, deepseek/deepseek-v4-pro), so any upstream provider can be used without code changes.

Quick start

Everything here needs one OpenRouter API key — it reaches Claude, Gemini, GPT, DeepSeek, and other models through a single endpoint, so you never need per-provider credentials.

PR summaries and AI review (GitHub Actions)

1. In the Lean repository you want to use this on, add the key as an Actions secret named OPENROUTER_KEY (Settings → Secrets and variables → Actions → New repository secret).
2. Add a workflow file to that repository:
   • PR summaries: copy the example workflow from summary/README.md to .github/workflows/pr_summary.yml.
   • AI review: copy the recommended ChatOps workflow from review/README.md to .github/workflows/ai-review.yml.
3. Open a pull request — a summary is posted (and refreshed on each push) as a PR comment. The review runs on demand: comment /review on the PR (a repo member — the review builds the PR's Lean with secrets in scope, so it is ChatOps-only by default).

Because the actions live in subdirectories of this repository, workflows reference them with a path:

- uses: alexanderlhicks/lean4repo-utils/summary@0.3   # or .../review@0.3
  with:
    github_token: ${{ secrets.GITHUB_TOKEN }}
    api_key: ${{ secrets.OPENROUTER_KEY }}
    ...

Each action's README documents every input: summary/README.md · review/README.md. The review action defaults to open-weight models — deep agents on z-ai/glm-5.2, an independent verification pass on a different family (deepseek/deepseek-v4-pro); any OpenRouter slug can be substituted.

sorry-tracker (CLI)

git clone https://github.com/alexanderlhicks/lean4repo-utils.git
cd lean4repo-utils/sorry-tracker

export OPENROUTER_API_KEY=sk-or-...
uv run sorry-tracker --repo-path /path/to/your/lean/project --dry-run

--dry-run previews the sorrys it finds, fully offline. Drop the flag to generate LLM analyses and open GitHub issues (requires an authenticated GitHub CLI: gh auth login). See sorry-tracker/README.md for all options.

Requirements

• Actions: nothing to install — the actions set up uv and Lean themselves on the runner. Your repository needs a working lake build (the review action builds the project to query the Lean toolchain).
• CLI / development: uv only; it provisions the right Python automatically (packages require Python ≥ 3.11, pinned to 3.12 via .python-version).

Development

This repository is a uv workspace; each tool is a member project with its own README and tests.

uv sync --all-packages        # one venv + one uv.lock at the workspace root

# Tests (per member, from its directory)
(cd common && uv run --no-sync pytest -q)
(cd sorry-tracker && uv run --no-sync pytest -q)
(cd summary && uv run --no-sync pytest -q)
(cd review && uv run --no-sync pytest -q)

uv run --no-sync ruff check . # lint everything

Dependency changes go in the member's pyproject.toml; re-lock with uv lock at the root (the actions install with --frozen). CI (.github/workflows/ci.yml) runs ruff, the four test suites, and validation of the two action.yml files on every PR.

License

Apache License 2.0.