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 CompPoly precedent step (algebraic naming + style-exception conventions) and grounds on spec_refs: docs/wiki; summary keeps validate_title + upstream_path: CompPoly/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

CI Workflow Overhaul: Migrate review & summary workflows to lean4repo-utils@0.3

This PR replaces the two main AI‑assisted PR workflows with fresh copies of the canonical examples from the lean4repo-utils READMEs, pinned at tag 0.3. The changes are entirely infrastructural: no Lean code, proofs, or mathematical content is touched.

Infrastructure / CI

• .github/workflows/review.yml — core change is the switch from the old alexanderlhicks/lean-review-workflow@main action to the new release‑pinned alexanderlhicks/lean4repo-utils/review@0.3. This removes the previous provider, model, external_refs, and repo_context_refs inputs and replaces them with a single spec_refs input set to 'docs/wiki'. The trigger is now strictly ChatOps (issue_comment type /review) — the previous pull_request trigger and its author‑association checks are removed. A new hard‑coded "Project precedent" block (CompPoly‑specific style/scope rules) is prepended to user instructions. The timeout increased from 90 to 120 minutes. The old structured comment parsing (External:/Internal:/Comments: sections) is replaced with a simple /review‑prefix strip.

• .github/workflows/summary.yml — migrated from alexanderlhicks/lean-summary-workflow@main to alexanderlhicks/lean4repo-utils/summary@0.3. The timeout-minutes: 20 setting is removed (falling back to action defaults). The additional_instructions_path input is removed because the action now reads CONTRIBUTING.md from the base ref by default. The comment block is expanded to explain the safety rationale for pull_request_target. All remaining inputs (permissions block, OPENROUTER_KEY, default model deepseek/deepseek-v4-flash) are retained.

• No sorry/admit placeholders were added (not applicable to CI workflows).

Key implications for reviewers:

• The summary workflow now runs on every PR via pull_request_target, never executing PR code; it is safe for external contributors.
• The review workflow is ChatOps‑only (requires /review from a repo member) and builds the PR with secrets in scope.
• Both workflows are intentionally fleet‑uniform, matching the README examples exactly. Any per‑repo tuning (model overrides, spec_refs, validate_title, upstream_path) is not included but is documented as actionable overlays in the action READMEs.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	97
❌ Lines Removed	130

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff modifies two CI workflow files (.github/workflows/review.yml and .github/workflows/summary.yml). The instructions provided are the CompPoly contribution guidelines. This diff does not change any .lean files, documentation files within docs/wiki/, or any of the formalization content that the guidelines primarily address. The changes are purely to CI/CD configuration and workflow logic. Therefore, the diff is irrelevant to the supplied instructions, which concern Lean code style, theorem naming, documentation, blueprint processes, and other formalization-specific practices.

---

📄 **Per-File Summaries**

• .github/workflows/review.yml: The workflow now triggers only on a /review comment (removed the pull_request trigger and the associated author-association checks), with a single issue_comment event type and a simplified concurrency group key. The timeout increased from 90 to 120 minutes. The comment‑parsing step was replaced: instead of extracting structured External:/Internal:/Comments: sections, it now strips the /review prefix and passes the remainder as free‑form instructions. A new Build review instructions step prepends a long, hard‑coded “Project precedent” block (detailing CompPoly‑specific naming, style exceptions, and scope rules) to the user’s text. The action used was switched from alexanderlhicks/lean-review-workflow@main (with Gemini API key and model) to alexanderlhicks/lean4repo-utils/review@0.3 (using OPENROUTER_KEY), which drops the old provider, model, external_refs, and repo_context_refs inputs and adds a new spec_refs input set to 'docs/wiki'.
• .github/workflows/summary.yml: Updated .github/workflows/summary.yml to use the release-pinned action alexanderlhicks/lean4repo-utils/summary@0.3 instead of the @main branch of the old lean-summary-workflow, and removed the timeout-minutes: 20 setting. The additional_instructions_path input was also removed (it is now the action's default behavior to read CONTRIBUTING.md from the base ref). The comment block was expanded to explain the safety rationale for using pull_request_target. Finally, the permissions block was retained but the inline comments were trimmed to only the essential justifications.

---

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

[github-actions]

Build Timing Report

• Commit: 54e0fde
• Message: Merge 45ab191 into 0ec1f6e
• Ref: chore/deploy-lean4repo-utils-0.2
• Comparison baseline: 860fd8a from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	384.41	373.43	-10.98	ok
Warm rebuild	1.59	1.34	-0.25	ok
Test path	34.68	35.61	+0.93	ok

Incremental Rebuild Signal

• Warm rebuild saved 372.09s vs clean (278.68x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
55.00	51.00	+4.00	CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
44.00	45.00	-1.00	CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
40.00	48.00	-8.00	CompPoly/Univariate/DivisionCorrectness.lean
39.00	33.00	+6.00	CompPoly/Fields/Binary/BF128Ghash/Impl.lean
24.00	31.00	-7.00	CompPoly/Bivariate/Deriv.lean
20.00	22.00	-2.00	CompPoly/Bivariate/ToPoly.lean
19.00	30.00	-11.00	CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Correctness.lean
18.00	17.00	+1.00	CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
17.00	18.00	-1.00	CompPoly/Univariate/Raw/Proofs.lean
16.00	16.00	+0.00	CompPoly/Fields/KoalaBear/Fast.lean
16.00	18.00	-2.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIT.lean
16.00	6.70	+9.30	CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean
16.00	15.00	+1.00	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Divisibility.lean
15.00	15.00	+0.00	CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
15.00	16.00	-1.00	CompPoly/Univariate/NTTFast/Correctness/Radix4DIF.lean
13.00	11.00	+2.00	CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
13.00	12.00	+1.00	CompPoly/Bivariate/Factor.lean
13.00	16.00	-3.00	CompPoly/Univariate/ReedSolomon/GaoCorrectness.lean
12.00	12.00	+0.00	CompPoly/Univariate/Basic.lean
12.00	11.00	+1.00	CompPoly/Fields/Binary/AdditiveNTT/Domain.lean