Skip to content

Commit f88b0a5

Browse files
author
leanprover-community-mathlib4-bot
committed
Trigger CI for leanprover/lean4#7565 
2 parents f278f81 + ed4fcff commit f88b0a5

688 files changed

Lines changed: 16314 additions & 11515 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/build.in.yml‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,14 @@ jobs:
3030
run: |
3131
find . -name . -o -prune -exec rm -rf -- {} +
3232
33-
- uses: actions/checkout@v4
33+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
3434

3535
# Run the case checker action
3636
- name: Check Case Sensitivity
37-
uses: credfeto/action-case-checker@v1.3.0
37+
uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
3838

3939
- name: Look for ignored files
40-
uses: credfeto/action-no-ignored-files@v1.2.0
40+
uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
4141

4242
- name: "Check for Lean files with the executable bit set"
4343
shell: bash
@@ -52,7 +52,7 @@ jobs:
5252
5353
- name: install Python
5454
if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
55-
uses: actions/setup-python@v5
55+
uses: actions/setup-python@42375524e23c412d93fb67b49958b491fce71c38 # v5.4.0
5656
with:
5757
python-version: 3.8
5858

@@ -96,7 +96,7 @@ jobs:
9696
9797
# The Hoskinson runners may not have jq installed, so do that now.
9898
- name: 'Setup jq'
99-
uses: dcarbone/install-jq-action@v2.1.0
99+
uses: dcarbone/install-jq-action@e397bd87438d72198f81efd21f876461183d383a # v3.0.1
100100

101101
- name: install elan
102102
run: |
@@ -105,7 +105,7 @@ jobs:
105105
./elan-init -y --default-toolchain none
106106
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
107107
108-
- uses: actions/checkout@v4
108+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
109109

110110
- name: If using a lean-pr-release toolchain, uninstall
111111
run: |
@@ -168,7 +168,7 @@ jobs:
168168
169169
- name: build mathlib
170170
id: build
171-
uses: liskin/gh-problem-matcher-wrap@v3
171+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
172172
with:
173173
linters: gcc
174174
run: |
@@ -270,7 +270,7 @@ jobs:
270270
run: lake exe graph
271271

272272
- name: upload the import graph
273-
uses: actions/upload-artifact@v4
273+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
274274
with:
275275
name: import-graph
276276
path: import_graph.dot
@@ -288,23 +288,23 @@ jobs:
288288
289289
- name: test mathlib
290290
id: test
291-
uses: liskin/gh-problem-matcher-wrap@v3
291+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
292292
with:
293293
linters: gcc
294294
run:
295295
lake --iofail test
296296

297297
- name: check for unused imports
298298
id: shake
299-
uses: liskin/gh-problem-matcher-wrap@v3
299+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
300300
with:
301301
linters: gcc
302302
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
303303

304304
- name: lint mathlib
305305
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
306306
id: lint
307-
uses: liskin/gh-problem-matcher-wrap@v3
307+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
308308
with:
309309
linters: gcc
310310
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
@@ -353,10 +353,10 @@ jobs:
353353
needs: [style_lint, build]
354354
runs-on: ubuntu-latest
355355
steps:
356-
- uses: actions/checkout@v4
356+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
357357

358358
- id: PR
359-
uses: 8BitJonny/gh-get-current-pr@3.0.0
359+
uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
360360
# TODO: this may not work properly if the same commit is pushed to multiple branches:
361361
# https://github.com/8BitJonny/gh-get-current-pr/issues/8
362362
with:
@@ -366,7 +366,7 @@ jobs:
366366

367367
- if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
368368
name: If `bench-after-CI` is present, add a `!bench` comment.
369-
uses: GrantBirki/comment@v2
369+
uses: GrantBirki/comment@f524ee31407667c05061bad41e1758b40298bd82 # v2.1.0
370370
with:
371371
token: ${{ secrets.AUTO_MERGE_TOKEN }}
372372
issue-number: ${{ steps.PR.outputs.number }}
@@ -384,7 +384,7 @@ jobs:
384384
385385
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
386386
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
387-
uses: GrantBirki/comment@v2
387+
uses: GrantBirki/comment@f524ee31407667c05061bad41e1758b40298bd82 # v2.1.0
388388
with:
389389
token: ${{ secrets.AUTO_MERGE_TOKEN }}
390390
issue-number: ${{ steps.PR.outputs.number }}

‎.github/workflows/PR_summary.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ jobs:
1010

1111
steps:
1212
- name: Checkout code
13-
uses: actions/checkout@v4
13+
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
1414
with:
1515
fetch-depth: 0
1616

@@ -36,7 +36,7 @@ jobs:
3636
fi
3737
3838
- name: Set up Python
39-
uses: actions/setup-python@v5
39+
uses: actions/setup-python@42375524e23c412d93fb67b49958b491fce71c38 # v5.4.0
4040
with:
4141
python-version: 3.12
4242

‎.github/workflows/actionlint.yml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,27 +10,27 @@ jobs:
1010
runs-on: ubuntu-latest
1111
steps:
1212
- name: Checkout
13-
uses: actions/checkout@v4
13+
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
1414

1515
- name: suggester / actionlint
16-
uses: reviewdog/action-actionlint@v1
16+
uses: reviewdog/action-actionlint@a5524e1c19e62881d79c1f1b9b6f09f16356e281 # v1.65.2
1717
with:
1818
tool_name: actionlint
19-
fail_on_error: true
19+
fail_level: error
2020

2121
check_build_yml:
2222
name: check workflows generated by build.in.yml
2323
runs-on: ubuntu-latest
2424
steps:
25-
- uses: actions/checkout@v4
25+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
2626

2727
- name: update workflows
2828
run: |
2929
cd .github/workflows/
3030
./mk_build_yml.sh
3131
3232
- name: suggester / build.in.yml
33-
uses: reviewdog/action-suggester@v1
33+
uses: reviewdog/action-suggester@4747dbc9f9e37adba0943e681cc20db466642158 # v1.21.0
3434
with:
3535
tool_name: mk_build_yml.sh
36-
fail_on_error: true
36+
fail_level: error

‎.github/workflows/add_label_from_diff.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ jobs:
2121
contents: read
2222
steps:
2323
- name: Checkout code
24-
uses: actions/checkout@v4
24+
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
2525
with:
2626
fetch-depth: 0
2727
- name: install elan

‎.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
./elan-init -y --default-toolchain none
1818
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
1919
20-
- uses: actions/checkout@v4
20+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
2121
with:
2222
ref: master
2323
sparse-checkout: |

‎.github/workflows/bors.yml‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,14 @@ jobs:
4040
run: |
4141
find . -name . -o -prune -exec rm -rf -- {} +
4242
43-
- uses: actions/checkout@v4
43+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
4444

4545
# Run the case checker action
4646
- name: Check Case Sensitivity
47-
uses: credfeto/action-case-checker@v1.3.0
47+
uses: credfeto/action-case-checker@cb652aeab29ed363bbdb7d9ee1bfcc010c46cac5 # v1.3.0
4848

4949
- name: Look for ignored files
50-
uses: credfeto/action-no-ignored-files@v1.2.0
50+
uses: credfeto/action-no-ignored-files@4fccae50720d89bef0cd9dc99a85a19b765d2e70 # v1.2.0
5151

5252
- name: "Check for Lean files with the executable bit set"
5353
shell: bash
@@ -62,7 +62,7 @@ jobs:
6262
6363
- name: install Python
6464
if: ${{ 'bors' == 'ubuntu-latest' }}
65-
uses: actions/setup-python@v5
65+
uses: actions/setup-python@42375524e23c412d93fb67b49958b491fce71c38 # v5.4.0
6666
with:
6767
python-version: 3.8
6868

@@ -106,7 +106,7 @@ jobs:
106106
107107
# The Hoskinson runners may not have jq installed, so do that now.
108108
- name: 'Setup jq'
109-
uses: dcarbone/install-jq-action@v2.1.0
109+
uses: dcarbone/install-jq-action@e397bd87438d72198f81efd21f876461183d383a # v3.0.1
110110

111111
- name: install elan
112112
run: |
@@ -115,7 +115,7 @@ jobs:
115115
./elan-init -y --default-toolchain none
116116
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
117117
118-
- uses: actions/checkout@v4
118+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
119119

120120
- name: If using a lean-pr-release toolchain, uninstall
121121
run: |
@@ -178,7 +178,7 @@ jobs:
178178
179179
- name: build mathlib
180180
id: build
181-
uses: liskin/gh-problem-matcher-wrap@v3
181+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
182182
with:
183183
linters: gcc
184184
run: |
@@ -280,7 +280,7 @@ jobs:
280280
run: lake exe graph
281281

282282
- name: upload the import graph
283-
uses: actions/upload-artifact@v4
283+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
284284
with:
285285
name: import-graph
286286
path: import_graph.dot
@@ -298,23 +298,23 @@ jobs:
298298
299299
- name: test mathlib
300300
id: test
301-
uses: liskin/gh-problem-matcher-wrap@v3
301+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
302302
with:
303303
linters: gcc
304304
run:
305305
lake --iofail test
306306

307307
- name: check for unused imports
308308
id: shake
309-
uses: liskin/gh-problem-matcher-wrap@v3
309+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
310310
with:
311311
linters: gcc
312312
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
313313

314314
- name: lint mathlib
315315
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
316316
id: lint
317-
uses: liskin/gh-problem-matcher-wrap@v3
317+
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
318318
with:
319319
linters: gcc
320320
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
@@ -363,10 +363,10 @@ jobs:
363363
needs: [style_lint, build]
364364
runs-on: ubuntu-latest
365365
steps:
366-
- uses: actions/checkout@v4
366+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
367367

368368
- id: PR
369-
uses: 8BitJonny/gh-get-current-pr@3.0.0
369+
uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
370370
# TODO: this may not work properly if the same commit is pushed to multiple branches:
371371
# https://github.com/8BitJonny/gh-get-current-pr/issues/8
372372
with:
@@ -376,7 +376,7 @@ jobs:
376376

377377
- if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
378378
name: If `bench-after-CI` is present, add a `!bench` comment.
379-
uses: GrantBirki/comment@v2
379+
uses: GrantBirki/comment@f524ee31407667c05061bad41e1758b40298bd82 # v2.1.0
380380
with:
381381
token: ${{ secrets.AUTO_MERGE_TOKEN }}
382382
issue-number: ${{ steps.PR.outputs.number }}
@@ -394,7 +394,7 @@ jobs:
394394
395395
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
396396
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
397-
uses: GrantBirki/comment@v2
397+
uses: GrantBirki/comment@f524ee31407667c05061bad41e1758b40298bd82 # v2.1.0
398398
with:
399399
token: ${{ secrets.AUTO_MERGE_TOKEN }}
400400
issue-number: ${{ steps.PR.outputs.number }}

‎.github/workflows/bot_fix_style.yaml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ jobs:
5858
5959
- id: user_permission
6060
if: steps.bot_fix_style.outputs.bot_fix_style == 'bot-fix-style'
61-
uses: actions-cool/check-user-permission@v2
61+
uses: actions-cool/check-user-permission@7b90a27f92f3961b368376107661682c441f6103 # v2.3.0
6262
with:
6363
require: 'write'
6464

@@ -71,7 +71,7 @@ jobs:
7171
# Is the `id` check a good way to check that this is a `comment`?
7272
if: ${{ steps.user_permission.outputs.require-result == 'true' &&
7373
! github.event.comment.id == '' }}
74-
uses: peter-evans/create-or-update-comment@v4
74+
uses: peter-evans/create-or-update-comment@71345be0265236311c031f5c7866368bd1eff043 # v4.0.0
7575
with:
7676
comment-id: ${{ github.event.comment.id }}
7777
reactions: rocket
@@ -95,7 +95,7 @@ jobs:
9595
run: |
9696
find . -name . -o -prune -exec rm -rf -- {} +
9797
98-
- uses: actions/checkout@v4
98+
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
9999
if: steps.user_permission.outputs.require-result == 'true'
100100
with:
101101
token: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
@@ -112,7 +112,7 @@ jobs:
112112

113113
- name: install Python
114114
if: steps.user_permission.outputs.require-result == 'true'
115-
uses: actions/setup-python@v5
115+
uses: actions/setup-python@42375524e23c412d93fb67b49958b491fce71c38 # v5.4.0
116116
with:
117117
python-version: 3.8
118118

0 commit comments

Comments
 (0)