Skip to content

Commit ae942d4

Browse files
author
leanprover-community-mathlib4-bot
committed
Trigger CI for leanprover/lean4#8070
2 parents 8edcf51 + 59c6079 commit ae942d4

3,242 files changed

Lines changed: 77094 additions & 40105 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.

.devcontainer/devcontainer.json

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
{
22
"name": "Mathlib4 dev container",
33

4-
"build": {
5-
"dockerfile": "Dockerfile"
6-
},
4+
"image": "ghcr.io/leanprover-community/mathlib4/gitpod",
75

86
"onCreateCommand": "lake exe cache get!",
97

.github/build.in.yml

Lines changed: 19 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -21,62 +21,6 @@ concurrency:
2121
cancel-in-progress: true
2222

2323
jobs:
24-
style_lint:
25-
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
26-
name: Lint styleJOB_NAME
27-
runs-on: STYLE_LINT_RUNNER
28-
steps:
29-
- name: cleanup
30-
run: |
31-
find . -name . -o -prune -exec rm -rf -- {} +
32-
33-
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
34-
35-
# Run the case checker action
36-
- name: Check Case Sensitivity
37-
uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
38-
39-
- name: Look for ignored files
40-
uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
41-
42-
- name: "Check for Lean files with the executable bit set"
43-
shell: bash
44-
run: |
45-
executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
46-
if [[ -n "$executable_files" ]]
47-
then
48-
echo "ERROR: The following Lean files have the executable bit set."
49-
echo "$executable_files"
50-
exit 1
51-
fi
52-
53-
- name: install Python
54-
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
55-
uses: actions/setup-python@8d9ed9ac5c53483de85588cdf95a591a75ab9f55 # v5.5.0
56-
with:
57-
python-version: 3.8
58-
59-
- name: Configure Lean
60-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
61-
with:
62-
auto-config: false
63-
use-github-cache: false
64-
use-mathlib-cache: false
65-
66-
- name: "run style linters"
67-
run: |
68-
lake exe lint-style
69-
70-
- name: Install bibtool
71-
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
72-
run: |
73-
sudo apt-get update
74-
sudo apt-get install -y bibtool
75-
76-
- name: lint references.bib
77-
run: |
78-
./scripts/lint-bib.sh
79-
8024
build:
8125
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
8226
name: BuildJOB_NAME
@@ -101,23 +45,12 @@ jobs:
10145
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
10246

10347
- name: Configure Lean
104-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
48+
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
10549
with:
10650
auto-config: false
10751
use-github-cache: false
10852
use-mathlib-cache: false
109-
110-
- name: If using a lean-pr-release toolchain, uninstall
111-
run: |
112-
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
113-
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
114-
elan toolchain uninstall "$(cat lean-toolchain)"
115-
fi
116-
117-
- name: print lean and lake versions
118-
run: |
119-
lean --version
120-
lake --version
53+
reinstall-transient-toolchain: true
12154

12255
- name: cleanup .cache/mathlib
12356
run: |
@@ -168,9 +101,9 @@ jobs:
168101
169102
- name: build mathlib
170103
id: build
171-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
104+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
172105
with:
173-
linters: gcc
106+
linters: lean
174107
run: |
175108
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
176109
@@ -205,7 +138,8 @@ jobs:
205138
cp ../lean-toolchain .
206139
MATHLIB_NO_CACHE_ON_UPDATE=1 lake update
207140
lake exe cache get || (sleep 1; lake exe cache get)
208-
lake build Plausible ProofWidgets
141+
# We need to run `lake build ProofWidgets` here to retrieve ProofWidgets via Reservoir.
142+
lake build ProofWidgets
209143
lake build --no-build Mathlib
210144
fi
211145
@@ -288,23 +222,23 @@ jobs:
288222
289223
- name: test mathlib
290224
id: test
291-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
225+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
292226
with:
293-
linters: gcc
227+
linters: lean
294228
run:
295229
lake --iofail test
296230

297231
- name: check for unused imports
298232
id: shake
299-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
233+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
300234
with:
301235
linters: gcc
302236
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
303237

304238
- name: lint mathlib
305239
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
306240
id: lint
307-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
241+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
308242
with:
309243
linters: gcc
310244
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
@@ -348,14 +282,21 @@ jobs:
348282
lake build
349283
lake -q exe lean4checker Lean4Checker
350284
285+
style_lint:
286+
name: Lint styleJOB_NAME
287+
runs-on: ubuntu-latest
288+
steps:
289+
- uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
290+
with:
291+
mode: check
292+
lint-bib-file: true
293+
351294
final:
352295
name: Post-CI jobJOB_NAME
353296
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
354297
needs: [style_lint, build]
355298
runs-on: ubuntu-latest
356299
steps:
357-
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
358-
359300
- id: PR
360301
uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
361302
# TODO: this may not work properly if the same commit is pushed to multiple branches:

.github/dependabot.yml

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,13 @@ updates:
88
schedule:
99
# Check for updates to GitHub Actions every month
1010
interval: "monthly"
11+
groups:
12+
# group updates into single PRs since we want to update both build.in.yml and its outputs at the same time
13+
actions-version-updates:
14+
applies-to: version-updates
15+
patterns:
16+
- "*"
17+
actions-security-updates:
18+
applies-to: security-updates
19+
patterns:
20+
- "*"

.github/workflows/PR_summary.yml

Lines changed: 90 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -31,12 +31,16 @@ jobs:
3131
# we use curl rather than octokit/request-action so that the job won't fail
3232
# (and send an annoying email) if the labels don't exist
3333
curl --request POST \
34-
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
35-
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
34+
--header 'Accept: application/vnd.github+json' \
35+
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
36+
--header 'X-GitHub-Api-Version: 2022-11-28' \
37+
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
38+
--data '{"labels":["merge-conflict"]}'
39+
3640
fi
3741
3842
- name: Set up Python
39-
uses: actions/setup-python@8d9ed9ac5c53483de85588cdf95a591a75ab9f55 # v5.5.0
43+
uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
4044
with:
4145
python-version: 3.12
4246

@@ -46,10 +50,61 @@ jobs:
4650
sudo apt-get install -y jq
4751
# If you have additional dependencies, install them here
4852
49-
- name: Get changed files
53+
- name: Get changed and removed/renamed files
5054
run: |
5155
git fetch origin ${{ github.base_ref }} # fetch the base branch
52-
git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt # get the list of changed files
56+
57+
# Get the list of all changed files.
58+
git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt
59+
60+
# Get all files which were removed or renamed.
61+
echo "Checking for removed files..."
62+
63+
# Shows the `D`eleted files, one per line.
64+
git diff --name-only --diff-filter D origin/${{ github.base_ref }}... | tee removed_files.txt
65+
echo "Checking for renamed files..."
66+
67+
# Shows the `R`enamed files, in human readable format
68+
# The `awk` pipe
69+
# * extracts into an array the old name as the key and the new name as the value
70+
# * eventually prints "`oldName` was renamed to `newName`" for each key-value pair.
71+
git diff -p --summary --diff-filter=R origin/${{ github.base_ref }}... |
72+
awk '
73+
/^rename from / {
74+
file=$0
75+
gsub(/rename from /, "", file)
76+
oldFile=file
77+
}
78+
/^rename to / {
79+
file=$0
80+
gsub(/rename to /, "", file)
81+
oldNew[oldFile]=file
82+
} END {
83+
for(old in oldNew) {
84+
printf("`%s` was renamed to `%s`\n", old, oldNew[old])
85+
}
86+
}' | tee renamed_files.txt
87+
88+
- name: Compute (re)moved files without deprecation
89+
run: |
90+
touch moved_without_deprecation.txt
91+
git checkout ${{ github.base_ref }}
92+
for file in $(cat removed_files.txt) ; do
93+
if grep ^deprecated_module "${file}" ; then
94+
printf 'info: removed file %s contains a deprecation\n' "${file}"
95+
else
96+
printf '\n⚠️ **warning**: file `%s` was removed without a module deprecation\n' "${file}" |
97+
tee -a moved_without_deprecation.txt
98+
fi
99+
done
100+
IFS=$'\n'
101+
for file in $(cat renamed_files.txt) ; do
102+
printf '\n⚠️ **warning**: file %s without a module deprecation\n' "${file}" |
103+
tee -a moved_without_deprecation.txt
104+
done
105+
106+
# we return to the PR branch, since the next step wants it!
107+
git checkout -
53108
54109
- name: Compute transitive imports
55110
run: |
@@ -69,6 +124,7 @@ jobs:
69124
70125
# switch back to the current branch: the `declarations_diff` script should be here
71126
git checkout "${currentHash}"
127+
72128
- name: Post or update the summary comment
73129
env:
74130
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
@@ -123,5 +179,34 @@ jobs:
123179
# store in a file, to avoid "long arguments" error.
124180
printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
125181
182+
# At the end, include any errors about removed or renamed files without deprecation.
183+
if [ -s moved_without_deprecation.txt ]
184+
then
185+
printf '\n\n---\n\n' >> please_merge_master.md
186+
cat moved_without_deprecation.txt >> please_merge_master.md
187+
fi
188+
126189
cat please_merge_master.md
127190
./scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
191+
192+
- name: Update the file-removed label
193+
run: |
194+
undeprecatedMoves="$(cat moved_without_deprecation.txt)"
195+
if [ -n "$undeprecatedMoves" ]; then
196+
echo "This PR has undeprecated module (re)movals."
197+
# we use curl rather than octokit/request-action so that the job won't fail
198+
# (and send an annoying email) if the labels don't exist
199+
curl --request POST \
200+
--header 'Accept: application/vnd.github+json' \
201+
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
202+
--header 'X-GitHub-Api-Version: 2022-11-28' \
203+
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
204+
--data '{"labels":["file-removed"]}'
205+
else
206+
echo "This PR (re)moves no modules without deprecations."
207+
# we use curl rather than octokit/request-action so that the job won't fail
208+
# (and send an annoying email) if the labels don't exist
209+
curl --request DELETE \
210+
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/file-removed \
211+
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
212+
fi

.github/workflows/add_label_from_diff.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
with:
2626
fetch-depth: 0
2727
- name: Configure Lean
28-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
28+
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
2929
with:
3030
auto-config: false
3131
use-github-cache: false

.github/workflows/bench_summary_comment.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ jobs:
1717
scripts/bench_summary.lean
1818
1919
- name: Configure Lean
20-
uses: leanprover/lean-action@f3ad22e9ca29cb9475bc9bee9afd1f39bb52bf6d # v1.1.2
20+
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
2121
with:
2222
auto-config: false
2323
use-github-cache: false

0 commit comments

Comments
 (0)