Skip to content

Commit 8d51910

Browse files
mans0954mans0954
committed
Merge branch 'master' into monotone_part_bind
2 parents 6fd1323 + 7733e60 commit 8d51910

File tree

2,726 files changed

+73204
-34085
lines changed

Some content is hidden

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

2,726 files changed

+73204
-34085
lines changed

‎.github/workflows/PR_summary.yml

+81
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
name: Post PR summary comment
2+
3+
on:
4+
pull_request:
5+
6+
jobs:
7+
build:
8+
runs-on: ubuntu-latest
9+
10+
steps:
11+
- name: Checkout code
12+
uses: actions/checkout@v4
13+
with:
14+
fetch-depth: 0
15+
16+
- name: Set up Python
17+
uses: actions/setup-python@v5
18+
with:
19+
python-version: 3.12
20+
21+
- name: Install dependencies
22+
run: |
23+
python -m pip install --upgrade pip
24+
sudo apt-get install -y jq
25+
# If you have additional dependencies, install them here
26+
27+
- name: Get changed files
28+
run: |
29+
git fetch origin ${{ github.base_ref }} # fetch the base branch
30+
git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt # get the list of changed files
31+
32+
- name: Compute transitive imports
33+
run: |
34+
# the checkout dance, to avoid a detached head
35+
git checkout master
36+
git checkout -
37+
currentHash="$(git rev-parse HEAD)"
38+
39+
# Compute the counts for the HEAD of the PR
40+
python ./scripts/count-trans-deps.py "Mathlib/" > head.json
41+
42+
# Checkout the merge base
43+
git checkout "$(git merge-base master ${{ github.sha }})"
44+
45+
# Compute the counts for the merge base
46+
python ./scripts/count-trans-deps.py "Mathlib/" > base.json
47+
48+
# switch back to the current branch: the `no_lost_declarations` script should be here
49+
git checkout "${currentHash}"
50+
- name: Post or update the summary comment
51+
env:
52+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
53+
BRANCH_NAME: ${{ github.head_ref }}
54+
run: |
55+
PR="${{ github.event.pull_request.number }}"
56+
title="### PR summary"
57+
58+
## Import count comment
59+
importCount=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
60+
if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ]
61+
then
62+
importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes" "${importCount}")"
63+
else
64+
importCount="$(printf '#### Import changes\n\n%s\n' "${importCount}")"
65+
fi
66+
67+
## Declarations' diff comment
68+
declDiff=$(./scripts/no_lost_declarations.sh short)
69+
if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
70+
then
71+
declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
72+
else
73+
declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")"
74+
fi
75+
git checkout "${BRANCH_NAME}"
76+
currentHash="$(git rev-parse HEAD)"
77+
hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
78+
79+
message="$(printf '%s [%s](%s)\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${importCount}" "${declDiff}")"
80+
81+
./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

‎.github/workflows/bors.yml

+13-44
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,14 @@ jobs:
5050
with:
5151
python-version: 3.8
5252

53-
- name: lint
53+
- name: install elan
54+
run: |
55+
set -o pipefail
56+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
57+
./elan-init -y --default-toolchain none
58+
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
59+
60+
- name: "run style linters: Python ones and their Lean rewrite"
5461
run: |
5562
./scripts/lint-style.sh
5663
@@ -64,24 +71,6 @@ jobs:
6471
run: |
6572
./scripts/lint-bib.sh
6673
67-
check_imported:
68-
if: github.repository == 'leanprover-community/mathlib4'
69-
name: Check all files imported
70-
runs-on: ubuntu-latest
71-
steps:
72-
- name: cleanup
73-
run: |
74-
find . -name . -o -prune -exec rm -rf -- {} +
75-
76-
- uses: actions/checkout@v4
77-
78-
- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
79-
run: |
80-
./scripts/mk_all.sh
81-
82-
- name: check that all files are imported
83-
run: git diff --exit-code
84-
8574
check_workflows:
8675
if: github.repository == 'leanprover-community/mathlib4'
8776
name: check workflows
@@ -101,23 +90,6 @@ jobs:
10190
- name: check that workflows were consistent
10291
run: git diff --exit-code
10392

104-
summarize_declarations:
105-
if: github.repository == 'leanprover-community/mathlib4'
106-
name: summarize_declarations
107-
runs-on: ubuntu-latest
108-
steps:
109-
- uses: actions/checkout@v4
110-
with:
111-
## fetch the whole repository, useful to find a common fork
112-
fetch-depth: 0
113-
- name: print_lost_declarations
114-
run: |
115-
## back and forth to settle a "detached head" (maybe?)
116-
git checkout -q master
117-
git checkout -q -
118-
printf '### Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
119-
./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
120-
12193
build:
12294
if: github.repository == 'leanprover-community/mathlib4'
12395
name: Build
@@ -142,18 +114,12 @@ jobs:
142114
- name: install elan
143115
run: |
144116
set -o pipefail
145-
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
117+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
146118
./elan-init -y --default-toolchain none
147119
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
148120
149121
- uses: actions/checkout@v4
150122

151-
# We update `Mathlib.lean` as a convenience here,
152-
# but verify that this didn't change anything in the `check_imported` job.
153-
- name: update Mathlib.lean
154-
run: |
155-
./scripts/mk_all.sh Mathlib
156-
157123
- name: If using a lean-pr-release toolchain, uninstall
158124
run: |
159125
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -166,6 +132,9 @@ jobs:
166132
lean --version
167133
lake --version
168134
135+
- name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
136+
run: lake exe mk_all --check
137+
169138
- name: build cache
170139
run: |
171140
lake build cache
@@ -319,7 +288,7 @@ jobs:
319288
final:
320289
name: Post-CI job
321290
if: github.repository == 'leanprover-community/mathlib4'
322-
needs: [style_lint, build, check_imported]
291+
needs: [style_lint, build]
323292
runs-on: ubuntu-latest
324293
steps:
325294
- uses: actions/checkout@v4

‎.github/workflows/build.yml

+13-44
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,14 @@ jobs:
5757
with:
5858
python-version: 3.8
5959

60-
- name: lint
60+
- name: install elan
61+
run: |
62+
set -o pipefail
63+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
64+
./elan-init -y --default-toolchain none
65+
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
66+
67+
- name: "run style linters: Python ones and their Lean rewrite"
6168
run: |
6269
./scripts/lint-style.sh
6370
@@ -71,24 +78,6 @@ jobs:
7178
run: |
7279
./scripts/lint-bib.sh
7380
74-
check_imported:
75-
if: github.repository == 'leanprover-community/mathlib4'
76-
name: Check all files imported
77-
runs-on: ubuntu-latest
78-
steps:
79-
- name: cleanup
80-
run: |
81-
find . -name . -o -prune -exec rm -rf -- {} +
82-
83-
- uses: actions/checkout@v4
84-
85-
- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
86-
run: |
87-
./scripts/mk_all.sh
88-
89-
- name: check that all files are imported
90-
run: git diff --exit-code
91-
9281
check_workflows:
9382
if: github.repository == 'leanprover-community/mathlib4'
9483
name: check workflows
@@ -108,23 +97,6 @@ jobs:
10897
- name: check that workflows were consistent
10998
run: git diff --exit-code
11099

111-
summarize_declarations:
112-
if: github.repository == 'leanprover-community/mathlib4'
113-
name: summarize_declarations
114-
runs-on: ubuntu-latest
115-
steps:
116-
- uses: actions/checkout@v4
117-
with:
118-
## fetch the whole repository, useful to find a common fork
119-
fetch-depth: 0
120-
- name: print_lost_declarations
121-
run: |
122-
## back and forth to settle a "detached head" (maybe?)
123-
git checkout -q master
124-
git checkout -q -
125-
printf '### Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
126-
./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
127-
128100
build:
129101
if: github.repository == 'leanprover-community/mathlib4'
130102
name: Build
@@ -149,18 +121,12 @@ jobs:
149121
- name: install elan
150122
run: |
151123
set -o pipefail
152-
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
124+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
153125
./elan-init -y --default-toolchain none
154126
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
155127
156128
- uses: actions/checkout@v4
157129

158-
# We update `Mathlib.lean` as a convenience here,
159-
# but verify that this didn't change anything in the `check_imported` job.
160-
- name: update Mathlib.lean
161-
run: |
162-
./scripts/mk_all.sh Mathlib
163-
164130
- name: If using a lean-pr-release toolchain, uninstall
165131
run: |
166132
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -173,6 +139,9 @@ jobs:
173139
lean --version
174140
lake --version
175141
142+
- name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
143+
run: lake exe mk_all --check
144+
176145
- name: build cache
177146
run: |
178147
lake build cache
@@ -326,7 +295,7 @@ jobs:
326295
final:
327296
name: Post-CI job
328297
if: github.repository == 'leanprover-community/mathlib4'
329-
needs: [style_lint, build, check_imported]
298+
needs: [style_lint, build]
330299
runs-on: ubuntu-latest
331300
steps:
332301
- uses: actions/checkout@v4

‎.github/workflows/build.yml.in

+13-44
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,14 @@ jobs:
3636
with:
3737
python-version: 3.8
3838

39-
- name: lint
39+
- name: install elan
40+
run: |
41+
set -o pipefail
42+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
43+
./elan-init -y --default-toolchain none
44+
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
45+
46+
- name: "run style linters: Python ones and their Lean rewrite"
4047
run: |
4148
./scripts/lint-style.sh
4249

@@ -50,24 +57,6 @@ jobs:
5057
run: |
5158
./scripts/lint-bib.sh
5259

53-
check_imported:
54-
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
55-
name: Check all files importedJOB_NAME
56-
runs-on: ubuntu-latest
57-
steps:
58-
- name: cleanup
59-
run: |
60-
find . -name . -o -prune -exec rm -rf -- {} +
61-
62-
- uses: actions/checkout@v4
63-
64-
- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
65-
run: |
66-
./scripts/mk_all.sh
67-
68-
- name: check that all files are imported
69-
run: git diff --exit-code
70-
7160
check_workflows:
7261
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
7362
name: check workflowsJOB_NAME
@@ -87,23 +76,6 @@ jobs:
8776
- name: check that workflows were consistent
8877
run: git diff --exit-code
8978

90-
summarize_declarations:
91-
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
92-
name: summarize_declarations
93-
runs-on: ubuntu-latest
94-
steps:
95-
- uses: actions/checkout@v4
96-
with:
97-
## fetch the whole repository, useful to find a common fork
98-
fetch-depth: 0
99-
- name: print_lost_declarations
100-
run: |
101-
## back and forth to settle a "detached head" (maybe?)
102-
git checkout -q master
103-
git checkout -q -
104-
printf '### Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
105-
./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
106-
10779
build:
10880
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
10981
name: BuildJOB_NAME
@@ -128,18 +100,12 @@ jobs:
128100
- name: install elan
129101
run: |
130102
set -o pipefail
131-
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
103+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
132104
./elan-init -y --default-toolchain none
133105
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
134106

135107
- uses: actions/checkout@v4
136108

137-
# We update `Mathlib.lean` as a convenience here,
138-
# but verify that this didn't change anything in the `check_imported` job.
139-
- name: update Mathlib.lean
140-
run: |
141-
./scripts/mk_all.sh Mathlib
142-
143109
- name: If using a lean-pr-release toolchain, uninstall
144110
run: |
145111
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -152,6 +118,9 @@ jobs:
152118
lean --version
153119
lake --version
154120

121+
- name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
122+
run: lake exe mk_all --check
123+
155124
- name: build cache
156125
run: |
157126
lake build cache
@@ -305,7 +274,7 @@ jobs:
305274
final:
306275
name: Post-CI jobJOB_NAME
307276
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
308-
needs: [style_lint, build, check_imported]
277+
needs: [style_lint, build]
309278
runs-on: ubuntu-latest
310279
steps:
311280
- uses: actions/checkout@v4

0 commit comments

Comments
 (0)