Skip to content

Commit af1c9f6

Browse files
author
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#13283 
2 parents 1cfc1b1 + 7aa60c9 commit af1c9f6

4,268 files changed

Lines changed: 59598 additions & 25715 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/build_template.yml‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,7 @@ jobs:
222222
223223
- name: validate lake-manifest.json inputRevs
224224
# Only enforce this on the main mathlib4 repository, not on nightly-testing
225-
if: github.repository == 'leanprover-community/mathlib4'
225+
if: github.repository == 'leanprover-community/mathlib4' && github.ref_name != 'nightly-testing'
226226
shell: bash
227227
run: |
228228
cd pr-branch
@@ -743,6 +743,12 @@ jobs:
743743
- name: clean up the import graph file
744744
run: rm import_graph.dot
745745

746+
- name: check all scripts build successfully
747+
run: |
748+
lake env lean scripts/create_deprecated_modules.lean
749+
lake env lean scripts/autolabel.lean
750+
lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
751+
746752
- name: build everything
747753
# make sure everything is available for test/import_all.lean
748754
# and that miscellaneous executables still work

‎.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

‎.github/workflows/olean_report_wf_run.yaml‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
# olean report (workflow_run)
2+
# Privileged counterpart of olean_report.yaml.
3+
#
4+
# Downloads the bridge artifact produced by olean_report.yaml and posts (or
5+
# updates) the olean diff as a comment on the PR. This workflow runs with
6+
# pull-requests: write permission so it can post comments even when the
7+
# triggering workflow ran in an unprivileged fork context.
8+
name: olean report (workflow_run)
9+
10+
on:
11+
workflow_run:
12+
workflows: ["olean report"]
13+
types:
14+
- completed
15+
16+
permissions:
17+
actions: read
18+
contents: read
19+
pull-requests: write
20+
21+
jobs:
22+
report:
23+
runs-on: ubuntu-latest
24+
if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }}
25+
steps:
26+
- name: Consume bridge artifact
27+
id: bridge
28+
uses: leanprover-community/privilege-escalation-bridge/consume@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
29+
with:
30+
token: ${{ github.token }}
31+
artifact: workflow-data
32+
source_workflow: olean report
33+
fail_on_missing: false
34+
extract: |
35+
pr_number=outputs.pr_number
36+
37+
- name: Find existing olean-report comment
38+
if: steps.bridge.outputs.pr_number != ''
39+
uses: peter-evans/find-comment@b30e6a3c0ed37e7c023ccd3f1db5c6c0b0c23aad # v4
40+
id: find-comment
41+
with:
42+
issue-number: ${{ steps.bridge.outputs.pr_number }}
43+
comment-author: 'github-actions[bot]'
44+
body-includes: '## Olean diff'
45+
46+
- name: Post or update olean-report comment
47+
if: steps.bridge.outputs.pr_number != ''
48+
uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
49+
with:
50+
comment-id: ${{ steps.find-comment.outputs.comment-id }}
51+
issue-number: ${{ steps.bridge.outputs.pr_number }}
52+
body-path: .bridge/comment_body.md
53+
edit-mode: replace

0 commit comments

Comments
 (0)