Skip to content

Commit 7851058

Browse files
david-christiansendavid-christiansen
authored
chore: improve PR status reporting (#495)
1 parent ab67394 commit 7851058

File tree

4 files changed

+265
-1
lines changed

4 files changed

+265
-1
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,7 @@ jobs:
8282
lake build figures
8383
8484
- name: Build
85+
id: build
8586
run: |
8687
lake build
8788
@@ -128,7 +129,6 @@ jobs:
128129
cat words.txt >> $GITHUB_STEP_SUMMARY
129130
echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
130131
131-
132132
- name: Set up Python for link checker
133133
if: github.event_name == 'push' || github.event_name == 'pull_request'
134134
uses: actions/setup-python@v4

‎.github/workflows/pr-testing.yml‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
on:
2+
push:
3+
branches:
4+
- main
5+
- 'lean-pr-testing-*'
6+
7+
name: "Report PR testing status to the lean4 repository"
8+
9+
jobs:
10+
build:
11+
name: Build site and generate HTML
12+
runs-on: ubuntu-latest
13+
14+
steps:
15+
- name: Install deps for figures (OS packages)
16+
run: |
17+
sudo apt update && sudo apt install -y poppler-utils
18+
19+
- name: Install deps for figures (TeX)
20+
uses: teatimeguest/setup-texlive-action@v3
21+
with:
22+
version: 2024
23+
packages: |
24+
scheme-small
25+
latex-bin
26+
fontspec
27+
standalone
28+
pgf
29+
pdftexcmds
30+
luatex85
31+
lualatex-math
32+
infwarerr
33+
ltxcmds
34+
xcolor
35+
fontawesome
36+
spath3
37+
inter
38+
epstopdf-pkg
39+
tex-gyre
40+
tex-gyre-math
41+
unicode-math
42+
amsmath
43+
sourcecodepro
44+
45+
- name: Do we have lualatex?
46+
run: |
47+
lualatex --version
48+
49+
- name: Install elan
50+
run: |
51+
set -o pipefail
52+
curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
53+
./elan-init -y --default-toolchain none
54+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
55+
56+
- uses: actions/checkout@v4
57+
58+
- name: Lean Version
59+
run: |
60+
lean --version
61+
62+
- name: Cache .lake
63+
uses: actions/cache/restore@v4
64+
with:
65+
path: .lake
66+
key: ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
67+
restore-keys: |
68+
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
69+
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}
70+
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-
71+
${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-
72+
73+
- name: Build figures
74+
run: |
75+
lake build figures
76+
77+
- name: Build
78+
id: build
79+
run: |
80+
lake build
81+
82+
- name: Save cache for .lake
83+
uses: actions/cache/save@v4
84+
with:
85+
path: .lake
86+
key: ${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lakefile.lean') }}-${{ github.sha }}
87+
88+
- name: Generate HTML (non-release)
89+
id: generate
90+
run: |
91+
lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single
92+
93+
- name: Report status to Lean PR
94+
if: always() && github.repository == 'leanprover/reference-manual'
95+
shell: bash
96+
env:
97+
TOKEN: ${{ secrets.LEAN_PR_TESTING }}
98+
GITHUB_CONTEXT: ${{ toJson(github) }}
99+
WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
100+
BUILD_OUTCOME: ${{ steps.build.outcome }}
101+
GENERATE_OUTCOME: ${{ steps.generate.outcome }}
102+
NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
103+
run: |
104+
scripts/lean-pr-testing-comments.sh lean

‎scripts/lean-pr-testing-comments.sh‎

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
## Create comments and labels on a Lean 4 PR after CI has finished on a `*-pr-testing-NNNN` branch.
2+
## This is based on the identically-named script in the Mathlib repository.
3+
4+
# Make this script robust against unintentional errors.
5+
# See e.g. http://redsymbol.net/articles/unofficial-bash-strict-mode/ for explanation.
6+
set -euo pipefail
7+
IFS=$'\n\t'
8+
9+
# Ensure the first argument is 'lean'
10+
if [ $# -eq 0 ]; then
11+
echo "No arguments provided"
12+
exit 1
13+
fi
14+
15+
# Set NIGHTLY_TESTING_REPO for comparison URLs (where the branches and tags actually live)
16+
if [ -z "${NIGHTLY_TESTING_REPO:-}" ]; then
17+
NIGHTLY_TESTING_REPO="leanprover/reference-manual"
18+
fi
19+
20+
# TODO: The whole script ought to be rewritten in javascript, to avoid having to use curl for API calls.
21+
#
22+
# This is not meant to be run from the command line, only from CI.
23+
# The inputs must be prepared as:
24+
# env:
25+
# TOKEN: ${{ secrets.LEAN_PR_TESTING }}
26+
# GITHUB_CONTEXT: ${{ toJson(github) }}
27+
# WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}
28+
# BUILD_OUTCOME: ${{ steps.build.outcome }}
29+
# GENERATE_OUTCOME: ${{ steps.test.outcome }}
30+
31+
# Adjust the branch pattern and URLs based on the repository.
32+
if [ "$1" == "lean" ]; then
33+
branch_prefix="lean-pr-testing"
34+
repo_url="https://api.github.com/repos/leanprover/lean4"
35+
base_branch="nightly-testing" # This really should be the relevant `nightly-testing-YYYY-MM-DD` tag.
36+
else
37+
echo "Unknown repository: $1. Must be 'lean'."
38+
exit 1
39+
fi
40+
41+
# Extract branch name and check if it matches the pattern.
42+
branch_name=$(echo "$GITHUB_CONTEXT" | jq -r .ref | cut -d'/' -f3)
43+
if [[ "$branch_name" =~ ^$branch_prefix-([0-9]+)$ ]]; then
44+
pr_number="${BASH_REMATCH[1]}"
45+
current_time=$(date "+%Y-%m-%d %H:%M:%S")
46+
47+
echo "This is a '$branch_prefix-$pr_number' branch, so we need to adjust labels and write a comment."
48+
49+
# Check if the PR has an awaiting-manual label
50+
has_awaiting_label=$(curl -L -s \
51+
-H "Accept: application/vnd.github+json" \
52+
-H "Authorization: Bearer $TOKEN" \
53+
-H "X-GitHub-Api-Version: 2022-11-28" \
54+
$repo_url/issues/$pr_number/labels | jq 'map(.name) | contains(["awaiting-manual"])')
55+
56+
# Perform actions based on outcomes
57+
if [ "$GENERATE_OUTCOME" == "success" ]; then
58+
echo "Removing label awaiting-manual"
59+
curl -L -s \
60+
-X DELETE \
61+
-H "Accept: application/vnd.github+json" \
62+
-H "Authorization: Bearer $TOKEN" \
63+
-H "X-GitHub-Api-Version: 2022-11-28" \
64+
$repo_url/issues/$pr_number/labels/awaiting-manual
65+
echo "Removing label breaks-manual"
66+
curl -L -s \
67+
-X DELETE \
68+
-H "Accept: application/vnd.github+json" \
69+
-H "Authorization: Bearer $TOKEN" \
70+
-H "X-GitHub-Api-Version: 2022-11-28" \
71+
$repo_url/issues/$pr_number/labels/breaks-manual
72+
echo "Adding label builds-manual"
73+
curl -L -s \
74+
-X POST \
75+
-H "Accept: application/vnd.github+json" \
76+
-H "Authorization: Bearer $TOKEN" \
77+
-H "X-GitHub-Api-Version: 2022-11-28" \
78+
$repo_url/issues/$pr_number/labels \
79+
-d '{"labels":["builds-manual"]}'
80+
elif [ "$GENERATE_OUTCOME" == "failure" ] || [ "$BUILD_OUTCOME" == "failure" ]; then
81+
echo "Removing label builds-manual"
82+
curl -L -s \
83+
-X DELETE \
84+
-H "Accept: application/vnd.github+json" \
85+
-H "Authorization: Bearer $TOKEN" \
86+
-H "X-GitHub-Api-Version: 2022-11-28" \
87+
$repo_url/issues/$pr_number/labels/builds-manual
88+
echo "Adding label breaks-manual"
89+
curl -L -s \
90+
-X POST \
91+
-H "Accept: application/vnd.github+json" \
92+
-H "Authorization: Bearer $TOKEN" \
93+
-H "X-GitHub-Api-Version: 2022-11-28" \
94+
$repo_url/issues/$pr_number/labels \
95+
-d '{"labels":["breaks-manual"]}'
96+
fi
97+
98+
branch="[$branch_prefix-$pr_number](https://github.com/$NIGHTLY_TESTING_REPO/compare/$base_branch...$branch_prefix-$pr_number)"
99+
# Depending on the success/failure, set the appropriate message
100+
if [ "GENERATE_OUTCOME" == "cancelled" ] || [ "$BUILD_OUTCOME" == "cancelled" ]; then
101+
message="- 🟡 Reference manual branch $branch build against this PR was cancelled. ($current_time) [View Log]($WORKFLOW_URL)"
102+
elif [ "$GENERATE_OUTCOME" == "success" ]; then
103+
message="- ✅ Reference manual branch $branch has successfully built against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
104+
elif [ "$BUILD_OUTCOME" == "failure" ]; then
105+
message="- 💥 Reference manual branch $branch build failed against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
106+
elif [ "$GENERATE_OUTCOME" == "failure" ]; then
107+
message="- ❌ Reference manual branch $branch built against this PR, but generating HTML failed. ($current_time) [View Log]($WORKFLOW_URL)"
108+
else
109+
message="- 🟡 Reference manual branch $branch build against this PR didn't complete normally. ($current_time) [View Log]($WORKFLOW_URL)"
110+
fi
111+
112+
echo "$message"
113+
114+
# Check if we should post a new comment or append to the existing one
115+
if [ "$has_awaiting_label" == "true" ]; then
116+
# Always post as a new comment if awaiting-manual label is present
117+
intro="Manual CI status:"
118+
echo "Posting as a separate comment due to awaiting-manual label at $repo_url/issues/$pr_number/comments"
119+
curl -L -s \
120+
-X POST \
121+
-H "Authorization: token $TOKEN" \
122+
-H "Accept: application/vnd.github.v3+json" \
123+
-d "$(jq --null-input --arg val "$message" '{"body": $val}')" \
124+
"$repo_url/issues/$pr_number/comments"
125+
else
126+
# Use existing behavior: append to existing comment or post a new one
127+
# Use GitHub API to check if a comment already exists
128+
existing_comment=$(curl -L -s -H "Authorization: token $TOKEN" \
129+
-H "Accept: application/vnd.github.v3+json" \
130+
"$repo_url/issues/$pr_number/comments" \
131+
| jq 'first(.[] | select(.body | test("^- . Manual") or startswith("Reference manual")) | select(.user.login == "leanprover-bot"))')
132+
existing_comment_id=$(echo "$existing_comment" | jq -r .id)
133+
existing_comment_body=$(echo "$existing_comment" | jq -r .body)
134+
135+
# Append new result to the existing comment or post a new comment
136+
if [ -z "$existing_comment_id" ]; then
137+
# Post new comment with a bullet point
138+
intro="Reference manual CI status:"
139+
echo "Posting as new comment at $repo_url/issues/$pr_number/comments"
140+
curl -L -s \
141+
-X POST \
142+
-H "Authorization: token $TOKEN" \
143+
-H "Accept: application/vnd.github.v3+json" \
144+
-d "$(jq --null-input --arg intro "$intro" --arg val "$message" '{"body": ($intro + "\n" + $val)}')" \
145+
"$repo_url/issues/$pr_number/comments"
146+
else
147+
# Append new result to the existing comment
148+
echo "Appending to existing comment at $repo_url/issues/$pr_number/comments"
149+
curl -L -s \
150+
-X PATCH \
151+
-H "Authorization: token $TOKEN" \
152+
-H "Accept: application/vnd.github.v3+json" \
153+
-d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$message" '{"body":($existing + "\n" + $message)}')" \
154+
"$repo_url/issues/comments/$existing_comment_id"
155+
fi
156+
fi
157+
else
158+
echo "Not reporting status because branch name '$branch_name' doesn't match ^$branch_prefix-([0-9]+)$"
159+
fi

‎test.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
This is a test

0 commit comments

Comments
 (0)