ci: deploy lean4repo-utils@0.3 PR review+summary (from README example)

[alexanderlhicks]

Deploys the two AI PR workflows on lean4repo-utils@0.3 with default models, built up from the canonical README example and then optimized for this repo.

Baseline (from the README example)

• review.yml → ChatOps-only (/review from a repo member), review@0.3, OPENROUTER_KEY.
• summary.yml → every-PR pull_request_target, summary@0.3, OPENROUTER_KEY, default model.

Repo-specific optimization

review restores the KB citation-join (maps changed .lean files to their cited docs/kb papers → spec_refs); summary keeps validate_title + upstream_path: ArkLib/ToMathlib/.

Trust model

• review is ChatOps-only — it builds the PR's Lean with secrets in scope, so it runs only when a member types /review.
• summary never executes PR code, so it is safe on every PR under pull_request_target.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

Given the PR's focus on CI infrastructure, the overview is best structured under the Infrastructure / CI header. The two workflow files are updated, each with specific modifications.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	12
❌ Lines Removed	11

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• .github/workflows/review.yml: Updated review.yml workflow to pin the OpenRouter review action from alexanderlhicks/lean4repo-utils/review@main to alexanderlhicks/lean4repo-utils/review@0.3, and updated the corresponding reference in the comment above the trigger from lean4repo-utils/review@main to lean4repo-utils/review@0.3. This ensures reproducible behavior by using a specific tagged version instead of a moving main branch.
• .github/workflows/summary.yml: In .github/workflows/summary.yml, the workflow action reference was updated from alexanderlhicks/lean-summary-workflow@main to alexanderlhicks/lean4repo-utils/summary@0.3. The timeout-minutes: 20 setting and the explicit additional_instructions_path: 'CONTRIBUTING.md' input were removed (the latter now defaults to CONTRIBUTING.md when unset). A multi-line comment was added explaining that the workflow is safe under pull_request_target because it never builds or executes PR code — it only reads the diff and committed source as data, and reads its policy file from the base ref. These changes matter because they pin the workflow to a versioned release, remove a redundant configuration that is now the default, and justify the continued use of pull_request_target for security-conscious reviewers.

---

Last updated: 2026-07-24 04:53 UTC.