Skip to content

Commit a8a11e8

Browse files
ryanncoderyanncode
committed
Resolve import conflict
2 parents 82c446a + 9e407aa commit a8a11e8

2,957 files changed

Lines changed: 31433 additions & 14685 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/actions/get-mathlib-ci/action.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ inputs:
1010
# Default pinned commit used by workflows unless they explicitly override.
1111
# Update this ref as needed to pick up changes to mathlib-ci scripts
1212
# This is also updated automatically by .github/workflows/update_dependencies.yml
13-
default: b6def9edd1c39de8602b8c177c66e9416e5dbc60
13+
default: d7b053bde8ef240c29f6724fa285dc5bb6bbe00a
1414
path:
1515
description: Checkout destination path.
1616
required: false

‎.github/workflows/nightly_detect_failure.yml‎

Lines changed: 23 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
type: 'stream'
2626
topic: 'Mathlib status updates'
2727
content: |
28-
❌ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
28+
❌ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.event.workflow_run.head_sha }}](https://github.com/${{ github.repository }}/commit/${{ github.event.workflow_run.head_sha }})).
2929
You can `git fetch; git checkout nightly-testing` and push a fix.
3030
3131
handle_success:
@@ -52,7 +52,10 @@ jobs:
5252
- name: Checkout code
5353
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
5454
with:
55-
ref: nightly-testing # checkout nightly-testing branch
55+
# Pin to the SHA whose CI just succeeded, not the current tip of `nightly-testing`,
56+
# which may have advanced while CI was running. Without this, the tag and
57+
# `nightly-testing-{green,daily}` updates below can point to an untested commit.
58+
ref: ${{ github.event.workflow_run.head_sha }}
5659
fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
5760
token: ${{ steps.app-token.outputs.token }}
5861
- name: Update the nightly-testing-green branch
@@ -73,13 +76,26 @@ jobs:
7376
if git ls-remote --tags --exit-code origin "nightly-testing-$version" >/dev/null; then
7477
printf 'Tag nightly-testing-%s already exists on the remote.' "${version}"
7578
else
76-
# If the tag does not exist, create and push the tag to remote
79+
# If the tag does not exist, create and push the tag to remote.
80+
# The `ls-remote` check above is racy: a concurrent run can push the
81+
# tag between our check and our push. Tolerate that case.
7782
printf 'Creating tag %s from the current state of the nightly-testing branch.' "nightly-testing-${version}"
7883
git tag "nightly-testing-${version}"
79-
git push origin "nightly-testing-${version}"
80-
# Update the tracking branches. With `--force` in case history gets rewritten on the `nightly-testing` branch.
81-
git push --force origin HEAD:nightly-testing-daily
82-
git push --force origin HEAD:nightly-testing-green
84+
if ! git push origin "nightly-testing-${version}"; then
85+
if git ls-remote --tags --exit-code origin "nightly-testing-${version}" >/dev/null; then
86+
printf 'Tag nightly-testing-%s was created concurrently; continuing.' "${version}"
87+
else
88+
exit 1
89+
fi
90+
fi
91+
# Fast-forward `nightly-testing-daily` and `nightly-testing-green` to the tested SHA.
92+
# Since we now pin to the SHA whose CI succeeded (which may be older than the current
93+
# tip of `nightly-testing` if a CI run for an older commit finishes after a newer one),
94+
# we must NOT force-push here, or we'd roll the tracking branches backwards.
95+
# If the push isn't a fast-forward, leave the branch alone; the daily force-push
96+
# job handles the rare case where `nightly-testing` history has been rewritten.
97+
git push origin HEAD:nightly-testing-daily || echo "Skipping nightly-testing-daily update: not a fast-forward."
98+
git push origin HEAD:nightly-testing-green || echo "Skipping nightly-testing-green update: not a fast-forward."
8399
hash="$(git rev-parse "nightly-testing-${version}")"
84100
curl -X POST "https://speed.lean-lang.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
85101
fi

‎.github/workflows/olean_report.yaml‎

Lines changed: 290 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,290 @@
1+
# olean report
2+
# On-demand olean diff for a PR, triggered by commenting `!olean_report`.
3+
# Compares oleans of the PR head against the merge base.
4+
#
5+
# This workflow runs with minimal permissions (contents: read only) so it is
6+
# safe to run code from fork PRs. The actual PR comment is posted by the
7+
# companion workflow olean_report_wf_run.yaml via the privilege-escalation
8+
# bridge.
9+
name: olean report
10+
11+
on:
12+
issue_comment:
13+
types: [created]
14+
15+
# cancel any in-progress run when a new comment arrives.
16+
concurrency:
17+
group: olean-report-${{ github.event.issue.number }}
18+
cancel-in-progress: true
19+
20+
permissions:
21+
contents: read
22+
23+
jobs:
24+
report:
25+
name: Prepare olean report
26+
runs-on: ubuntu-latest
27+
# Skip if comment does not contain the trigger word.
28+
if: >-
29+
${{
30+
github.repository == 'leanprover-community/mathlib4' &&
31+
github.event.issue.pull_request != null &&
32+
github.event.issue.state == 'open' &&
33+
contains(github.event.comment.body, '!olean_report')
34+
}}
35+
steps:
36+
- name: Check trigger pattern
37+
id: check_trigger
38+
env:
39+
COMMENT_BODY: ${{ github.event.comment.body }}
40+
run: |
41+
# Require !olean_report to appear at the beginning of a line.
42+
if printf '%s' "$COMMENT_BODY" | grep -qE '^!olean_report'; then
43+
echo "triggered=true" >> "$GITHUB_OUTPUT"
44+
else
45+
echo "triggered=false" >> "$GITHUB_OUTPUT"
46+
echo "'!olean_report' was not found at the beginning of a line; skipping."
47+
fi
48+
49+
- name: Checkout local actions
50+
if: steps.check_trigger.outputs.triggered == 'true'
51+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
52+
with:
53+
ref: ${{ github.workflow_sha }}
54+
fetch-depth: 1
55+
sparse-checkout: .github/actions
56+
path: workflow-actions
57+
58+
- name: Get mathlib-ci
59+
if: steps.check_trigger.outputs.triggered == 'true'
60+
uses: ./workflow-actions/.github/actions/get-mathlib-ci
61+
62+
# We use the GH CLI here because issue_comment events do not carry the
63+
# full pull_request payload.
64+
- name: Get PR info
65+
id: pr_info
66+
if: steps.check_trigger.outputs.triggered == 'true'
67+
env:
68+
GH_TOKEN: ${{ github.token }}
69+
run: |
70+
pr_json=$(gh pr view "${{ github.event.issue.number }}" \
71+
--repo "${{ github.repository }}" \
72+
--json headRefOid,baseRefOid,baseRefName)
73+
{
74+
echo "head_sha=$(echo "$pr_json" | jq -r '.headRefOid')"
75+
echo "base_sha=$(echo "$pr_json" | jq -r '.baseRefOid')"
76+
echo "base_ref=$(echo "$pr_json" | jq -r '.baseRefName')"
77+
} >> "$GITHUB_OUTPUT"
78+
79+
# Using refs/pull/N/head works for both same-repo and fork PRs, since
80+
# GitHub mirrors fork commits under this ref.
81+
# We fetch full depth so that we can compute the merge base.
82+
- name: Checkout PR head
83+
if: steps.check_trigger.outputs.triggered == 'true'
84+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
85+
with:
86+
repository: ${{ github.repository }}
87+
ref: refs/pull/${{ github.event.issue.number }}/head
88+
fetch-depth: 0
89+
path: pr-branch
90+
91+
# Check out master into tools-branch. We build the `cache` binary from
92+
# here so that a single binary can fetch oleans for both checkouts.
93+
- name: Checkout tools branch (master)
94+
if: steps.check_trigger.outputs.triggered == 'true'
95+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
96+
with:
97+
repository: ${{ github.repository }}
98+
ref: master
99+
fetch-depth: 1
100+
path: tools-branch
101+
102+
# Using the merge base rather than the base-branch tip avoids spurious
103+
# differences caused by commits that landed on master after this PR
104+
# branched off.
105+
- name: Compute merge base
106+
id: merge_base
107+
if: steps.check_trigger.outputs.triggered == 'true'
108+
working-directory: pr-branch
109+
run: |
110+
BASE_SHA="${{ steps.pr_info.outputs.base_sha }}"
111+
git fetch --depth=1 origin "$BASE_SHA"
112+
MERGE_BASE=$(git merge-base HEAD FETCH_HEAD)
113+
echo "sha=$MERGE_BASE" >> "$GITHUB_OUTPUT"
114+
115+
- name: Checkout merge base
116+
if: steps.check_trigger.outputs.triggered == 'true'
117+
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
118+
with:
119+
repository: ${{ github.repository }}
120+
ref: ${{ steps.merge_base.outputs.sha }}
121+
fetch-depth: 1
122+
path: base
123+
124+
- name: Check toolchain compatibility
125+
id: toolchain_check
126+
if: steps.check_trigger.outputs.triggered == 'true'
127+
env:
128+
BASE_REF: ${{ steps.pr_info.outputs.base_ref }}
129+
run: |
130+
PR_TC=$(cat pr-branch/lean-toolchain)
131+
BASE_TC=$(cat base/lean-toolchain)
132+
TOOLS_TC=$(cat tools-branch/lean-toolchain)
133+
MATCH=true
134+
MISMATCH_REASON=
135+
if [ "$PR_TC" != "$BASE_TC" ]; then
136+
MATCH=false
137+
MISMATCH_REASON=pr_vs_base
138+
elif [ "$BASE_REF" = "master" ] && [ "$TOOLS_TC" != "$PR_TC" ]; then
139+
# it's unlikely we'll be in a situation where we run this against a PR not into master
140+
# but just in case, we will allow them to have a different toolchain from the tools branch (master)
141+
MATCH=false
142+
MISMATCH_REASON=tools_vs_pr
143+
fi
144+
{
145+
echo "pr_toolchain=$PR_TC"
146+
echo "base_toolchain=$BASE_TC"
147+
echo "tools_toolchain=$TOOLS_TC"
148+
echo "match=$MATCH"
149+
if [ -n "$MISMATCH_REASON" ]; then echo "mismatch_reason=$MISMATCH_REASON"; fi
150+
} >> "$GITHUB_OUTPUT"
151+
152+
# We use --default-toolchain none so elan itself does not download a
153+
# toolchain at install time; the toolchain is resolved lazily when
154+
# `lake` runs inside tools-branch.
155+
- name: Install elan
156+
if: steps.toolchain_check.outputs.match == 'true'
157+
shell: bash
158+
run: |
159+
curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh
160+
chmod +x elan-init.sh
161+
./elan-init.sh -y --default-toolchain none
162+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
163+
164+
- name: Build cache binary
165+
if: steps.toolchain_check.outputs.match == 'true'
166+
run: |
167+
cd tools-branch
168+
lake build cache
169+
echo "CACHE_BIN=$(pwd)/.lake/build/bin/cache" >> "$GITHUB_ENV"
170+
171+
- name: Fetch PR head oleans
172+
id: pr_oleans
173+
if: steps.toolchain_check.outputs.match == 'true'
174+
continue-on-error: true
175+
run: |
176+
cd pr-branch
177+
lake env "$CACHE_BIN" get
178+
179+
- name: Check PR head oleans
180+
id: pr_oleans_check
181+
if: steps.toolchain_check.outputs.match == 'true'
182+
run: |
183+
if find pr-branch/.lake/build/lib/lean/Mathlib \
184+
-name '*.olean' -print -quit 2>/dev/null | grep -q .; then
185+
echo "available=true" >> "$GITHUB_OUTPUT"
186+
else
187+
echo "available=false" >> "$GITHUB_OUTPUT"
188+
fi
189+
190+
# Fetch oleans for the merge base (only if the PR head oleans are present,
191+
# to avoid wasting time when the PR hasn't been built yet).
192+
- name: Fetch merge base oleans
193+
id: base_oleans
194+
if: steps.pr_oleans_check.outputs.available == 'true'
195+
continue-on-error: true
196+
run: |
197+
cd base
198+
lake env "$CACHE_BIN" get
199+
200+
- name: Generate olean report
201+
if: steps.check_trigger.outputs.triggered == 'true'
202+
env:
203+
TOOLCHAINS_MATCH: ${{ steps.toolchain_check.outputs.match }}
204+
MISMATCH_REASON: ${{ steps.toolchain_check.outputs.mismatch_reason }}
205+
PR_TOOLCHAIN: ${{ steps.toolchain_check.outputs.pr_toolchain }}
206+
BASE_TOOLCHAIN: ${{ steps.toolchain_check.outputs.base_toolchain }}
207+
TOOLS_TOOLCHAIN: ${{ steps.toolchain_check.outputs.tools_toolchain }}
208+
PR_OLEANS_OK: ${{ steps.pr_oleans_check.outputs.available }}
209+
MERGE_BASE_SHA: ${{ steps.merge_base.outputs.sha }}
210+
BASE_REF: ${{ steps.pr_info.outputs.base_ref }}
211+
ACTIONS_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
212+
run: |
213+
if [ "$TOOLCHAINS_MATCH" != "true" ]; then
214+
if [ "$MISMATCH_REASON" = "tools_vs_pr" ]; then
215+
cat > comment_body.md << MDEOF
216+
## Olean diff
217+
218+
**Lean toolchain mismatch — \`master\` has bumped the toolchain.**
219+
220+
The PR and its merge base use \`${PR_TOOLCHAIN}\` but \`master\` uses \`${TOOLS_TOOLCHAIN}\`.
221+
Please merge \`master\` into your PR branch before requesting an olean report.
222+
223+
[CI run](${ACTIONS_URL})
224+
MDEOF
225+
else
226+
cat > comment_body.md << MDEOF
227+
## Olean diff
228+
229+
**Lean toolchain mismatch — oleans are not comparable.**
230+
231+
The merge base uses \`${BASE_TOOLCHAIN}\` but the PR head uses \`${PR_TOOLCHAIN}\`.
232+
Oleans compiled by different Lean versions are binary-incompatible; the diff would show every file as changed.
233+
234+
[CI run](${ACTIONS_URL})
235+
MDEOF
236+
fi
237+
elif [ "$PR_OLEANS_OK" != "true" ]; then
238+
cat > comment_body.md << 'MDEOF'
239+
## Olean diff
240+
241+
**Oleans for this PR are not yet available in the cache.**
242+
243+
Possible reasons:
244+
- The CI build for this commit has not finished yet.
245+
Wait for the build to complete, then post `!olean_report` again.
246+
- The CI build failed or was cancelled.
247+
Fix any errors and push a new commit.
248+
- The cache upload step was skipped.
249+
250+
Check the [CI run]($ACTIONS_URL) and the Actions tab for this PR's build status.
251+
MDEOF
252+
# expand $ACTIONS_URL in the heredoc output
253+
sed -i "s|\$ACTIONS_URL|${ACTIONS_URL}|g" comment_body.md
254+
else
255+
python3 "${CI_SCRIPTS_DIR}/pr_summary/olean_diff.py" \
256+
base/.lake/build/lib/lean \
257+
pr-branch/.lake/build/lib/lean \
258+
comment_body.md \
259+
olean_diff_full.txt \
260+
--merge-base-sha "${MERGE_BASE_SHA}" \
261+
--base-ref "${BASE_REF}" \
262+
--actions-url "${ACTIONS_URL}"
263+
fi
264+
265+
- name: Upload full olean diff
266+
if: steps.check_trigger.outputs.triggered == 'true'
267+
uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
268+
with:
269+
name: olean-diff-full
270+
path: olean_diff_full.txt
271+
if-no-files-found: ignore
272+
retention-days: 5
273+
274+
- name: Prepare bridge outputs
275+
if: steps.check_trigger.outputs.triggered == 'true'
276+
run: |
277+
jq -n \
278+
--arg pr_number "${{ github.event.issue.number }}" \
279+
'{ pr_number: $pr_number }' > bridge-outputs.json
280+
281+
- name: Emit bridge artifact
282+
if: steps.check_trigger.outputs.triggered == 'true'
283+
uses: leanprover-community/privilege-escalation-bridge/emit@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
284+
with:
285+
artifact: workflow-data
286+
outputs_file: bridge-outputs.json
287+
include_event: minimal
288+
files: |
289+
comment_body.md
290+
retention_days: 5

0 commit comments

Comments
 (0)