Skip to content

Commit 3e77ada

Browse files
alexanderlhicksclaude
alexanderlhicks
and
claude
committed
ci: deploy lean4repo-utils@0.3 review+summary from the README example
Regenerate both AI PR workflows as fresh copies of the canonical example workflows in the action READMEs, pinned @0.3, using default models: - review: ChatOps-only (/review from a repo member), review@0.3, OPENROUTER_KEY. - summary: every-PR pull_request_target, summary@0.3, OPENROUTER_KEY, default model. Supersedes the earlier per-repo migration so every fleet repo runs the identical, current, example-based workflow. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 0ec1f6e commit 3e77ada

2 files changed

Lines changed: 74 additions & 141 deletions

File tree

‎.github/workflows/review.yml‎

Lines changed: 60 additions & 130 deletions
Original file line numberDiff line numberDiff line change
@@ -1,130 +1,60 @@
1-
name: PR Review
2-
3-
on:
4-
pull_request:
5-
types: [opened]
6-
issue_comment:
7-
types: [created]
8-
9-
concurrency:
10-
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.event.issue.number }}
11-
cancel-in-progress: true
12-
13-
jobs:
14-
review:
15-
if: >-
16-
(
17-
github.event_name == 'pull_request' &&
18-
(
19-
github.event.pull_request.author_association == 'OWNER' ||
20-
github.event.pull_request.author_association == 'MEMBER' ||
21-
github.event.pull_request.author_association == 'COLLABORATOR'
22-
)
23-
) ||
24-
(
25-
github.event_name == 'issue_comment' &&
26-
github.event.issue.pull_request &&
27-
startsWith(github.event.comment.body, '/review') &&
28-
(
29-
github.event.comment.author_association == 'OWNER' ||
30-
github.event.comment.author_association == 'MEMBER' ||
31-
github.event.comment.author_association == 'COLLABORATOR'
32-
)
33-
)
34-
runs-on: ubuntu-latest
35-
timeout-minutes: 90
36-
permissions:
37-
contents: read
38-
pull-requests: write
39-
steps:
40-
- name: Extract arguments from comment
41-
id: get_args
42-
if: github.event_name == 'issue_comment'
43-
env:
44-
COMMENT_BODY: ${{ github.event.comment.body }}
45-
run: |
46-
EOF=$(openssl rand -hex 8)
47-
48-
awk -v eof="$EOF" -v gh_out="$GITHUB_OUTPUT" '
49-
BEGIN {
50-
ext = ""
51-
repo = ""
52-
com = ""
53-
section = ""
54-
}
55-
/^External:/ { section="ext"; next }
56-
/^Internal:/ { section="repo"; next }
57-
/^Comments:/ { section="com"; next }
58-
{
59-
gsub(/\r/, "", $0);
60-
gsub(/^[ \t]+|[ \t]+$/, "", $0);
61-
if ($0 == "" || $0 == "/review") { next }
62-
63-
if (section == "ext") {
64-
sub(/^- +/, "");
65-
if (ext != "") { ext = ext "," $0 } else { ext = $0 }
66-
}
67-
else if (section == "repo") {
68-
sub(/^- +/, "");
69-
if (repo != "") { repo = repo "," $0 } else { repo = $0 }
70-
}
71-
else if (section == "com") {
72-
if (com != "") { com = com "\n" $0 } else { com = $0 }
73-
}
74-
}
75-
END {
76-
printf "external_refs=%s\n", ext >> gh_out
77-
printf "repo_context_refs=%s\n", repo >> gh_out
78-
printf "additional_comments<<%s\n", eof >> gh_out
79-
printf "%s\n", com >> gh_out
80-
printf "%s\n", eof >> gh_out
81-
}
82-
' <<< "$COMMENT_BODY"
83-
shell: bash
84-
85-
- name: Build review instructions
86-
id: build_instructions
87-
env:
88-
USER_COMMENTS: ${{ steps.get_args.outputs.additional_comments }}
89-
run: |
90-
EOF=$(openssl rand -hex 8)
91-
{
92-
echo "final<<${EOF}"
93-
cat <<'PRECEDENT'
94-
Project precedent (CompPoly-specific conventions that override generic CONTRIBUTING.md rules — do NOT flag these as violations):
95-
96-
Variable naming overrides (algebraic context):
97-
- Algebraic carrier types use R, M, G, F (rings, modules, groups, fields), not α, β.
98-
- Polynomial-typed values use p, q (e.g. CPolynomial, CMvPolynomial, CMlPolynomial), not just predicates.
99-
- Indices into vectors, lists, and Fin n use i, j, k regardless of underlying numeric type.
100-
- In algebraic lemma names that mirror Mathlib (e.g. pow_add, npow_add), exponent variables may be a, b.
101-
102-
Style rules marked "preferred but not enforced" in CONTRIBUTING.md (the merged codebase uses both styles freely — do not flag):
103-
- "Use the where syntax for instances" — both `instance ... := ⟨...⟩` and `instance ... where` are accepted.
104-
- "Use manual dot notation for equality" — both `h.symm` and `Eq.symm h` are accepted.
105-
- "Use <| / |> to reduce nesting" — both pipe-style and parens are accepted.
106-
107-
File scope of style rules:
108-
- The 100-character line-length rule applies ONLY to `.lean` source files. Do NOT flag long lines in `.md`, `.yml`, `.toml`, or any other non-Lean files. The enforced linter (`scripts/lint-style.py`) only processes `.lean` files.
109-
110-
Review scope:
111-
- Flag ONLY lines introduced by this PR (the diff). Do not comment on pre-existing code that this PR did not modify.
112-
PRECEDENT
113-
if [ -n "${USER_COMMENTS}" ]; then
114-
printf '\n\nUser-supplied additional context:\n%s\n' "${USER_COMMENTS}"
115-
fi
116-
echo "${EOF}"
117-
} >> $GITHUB_OUTPUT
118-
shell: bash
119-
120-
- uses: alexanderlhicks/lean-review-workflow@main
121-
with:
122-
github_token: ${{ secrets.GITHUB_TOKEN }}
123-
api_key: ${{ secrets.GEMINI_API_KEY }}
124-
provider: gemini
125-
model: gemini-3.1-pro-preview
126-
pr_number: ${{ github.event.issue.number || github.event.pull_request.number }}
127-
external_refs: "${{ steps.get_args.outputs.external_refs }}"
128-
repo_context_refs: "${{ steps.get_args.outputs.repo_context_refs }}"
129-
additional_comments: "${{ steps.build_instructions.outputs.final }}"
130-
1+
name: PR Review
2+
3+
# Review runs ONLY on demand, via a `/review` comment from a repo member. It is
4+
# deliberately NOT run on PR open: the review path builds and elaborates the
5+
# PR's Lean code with the OpenRouter secret and a write token in scope, so until
6+
# the two-stage secret-free split (S2) lands, running it is safe only for code a
7+
# trusted maintainer has chosen to review. See the review action README.
8+
on:
9+
issue_comment:
10+
types: [created]
11+
12+
concurrency:
13+
group: ${{ github.workflow }}-${{ github.event.issue.number }}
14+
cancel-in-progress: true
15+
16+
jobs:
17+
review:
18+
# The COMMENT author (not the PR author) is the trust boundary.
19+
if: >-
20+
github.event_name == 'issue_comment' &&
21+
github.event.issue.pull_request &&
22+
startsWith(github.event.comment.body, '/review') &&
23+
(
24+
github.event.comment.author_association == 'OWNER' ||
25+
github.event.comment.author_association == 'MEMBER' ||
26+
github.event.comment.author_association == 'COLLABORATOR'
27+
)
28+
runs-on: ubuntu-latest
29+
timeout-minutes: 120
30+
permissions:
31+
contents: read
32+
pull-requests: write
33+
steps:
34+
# Everything after `/review` is freeform focus text; URLs and existing
35+
# repo paths it mentions become review context automatically.
36+
- name: Extract instructions from /review comment
37+
id: get_args
38+
env:
39+
COMMENT_BODY: ${{ github.event.comment.body }}
40+
run: |
41+
EOF=$(openssl rand -hex 8)
42+
{
43+
echo "instructions<<$EOF"
44+
printf '%s\n' "$COMMENT_BODY" | sed -E '1s|^/review[[:space:]]*||'
45+
echo "$EOF"
46+
} >> "$GITHUB_OUTPUT"
47+
shell: bash
48+
49+
- uses: alexanderlhicks/lean4repo-utils/review@0.3
50+
with:
51+
github_token: ${{ secrets.GITHUB_TOKEN }}
52+
api_key: ${{ secrets.OPENROUTER_KEY }}
53+
pr_number: ${{ github.event.issue.number }}
54+
# URLs and repo paths mentioned in the /review comment are extracted
55+
# into external/spec/repo context automatically.
56+
additional_comments: "${{ steps.get_args.outputs.instructions }}"
57+
# Everything else uses the action defaults (deep agents on z-ai/glm-5.2,
58+
# verification on deepseek/deepseek-v4-pro, lean_tools + verify_findings
59+
# on). See the review action README to override models or tune
60+
# spec_refs / escape_hatch_allowlist / dependent_impact_max.

‎.github/workflows/summary.yml‎

Lines changed: 14 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,10 @@
11
name: 'PR Summary'
22

3+
# Summary runs on every PR update (open + each new commit). It is SAFE under
4+
# pull_request_target — where the OpenRouter secret and a write token are in
5+
# scope even for fork PRs — because it never builds or executes PR code: it
6+
# reads the diff and committed source as data, and reads its policy file from
7+
# the BASE ref (S4). See the summary action README.
38
on:
49
pull_request_target:
510
types: [opened, synchronize, reopened]
@@ -9,25 +14,23 @@ concurrency:
914
cancel-in-progress: true
1015

1116
permissions:
12-
contents: read # required: the action checks out the PR head to read the diff
13-
pull-requests: write # required: post/update the summary comment
14-
issues: read # optional: link affected sorries to `proof wanted` issues
17+
contents: read
18+
pull-requests: write
19+
issues: read
1520

1621
jobs:
1722
summarize:
1823
runs-on: ubuntu-latest
19-
timeout-minutes: 20
2024
steps:
2125
- name: Generate PR Summary
22-
uses: alexanderlhicks/lean-summary-workflow@main
26+
uses: alexanderlhicks/lean4repo-utils/summary@0.3
2327
with:
2428
github_token: ${{ secrets.GITHUB_TOKEN }}
2529
api_key: ${{ secrets.OPENROUTER_KEY }}
26-
# model: inherits the action default (deepseek/deepseek-v4-flash).
27-
# Set `model: <openrouter-slug>` here to override for this repo only.
2830
github_repository: ${{ github.repository }}
2931
pr_number: ${{ github.event.pull_request.number }}
30-
additional_instructions_path: 'CONTRIBUTING.md'
31-
validate_title: 'true'
32-
upstream_path: 'CompPoly/ToMathlib/'
33-
# Other optional knobs (reasoning_effort, max_*_diff_chars): see the action README.
32+
# Uses the default model (deepseek/deepseek-v4-flash). Optional knobs:
33+
# model: <any OpenRouter slug> # e.g. google/gemini-3-flash-preview
34+
# additional_instructions_path: 'CONTRIBUTING.md' # default; read from the base ref
35+
# validate_title: 'true' # enforce conventional-commit PR titles
36+
# upstream_path: 'ToMathlib/' # remind on changes under this prefix

0 commit comments

Comments
 (0)