Skip to content

Commit eaa95ed

Browse files
adomaniRida-Hamadani
authored andcommitted
CI: install elan in lint_and_suggest, suggest import changes (#15250)
The `lint` step in [this action](https://github.com/leanprover-community/mathlib4/actions/runs/10137312257/job/28027367787?pr=15250) used to fail. Also added reviewdog suggestion to propose adding missing `import`s in "import all" files. #15251 tests that the step can fail and the reviewdog suggests changes to `Mathlib.lean`. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/silent.20CI.20lint.20error/near/454527007)
1 parent f8de0a4 commit eaa95ed

File tree

1 file changed

+10
-2
lines changed

1 file changed

+10
-2
lines changed

.github/workflows/lint_and_suggest_pr.yml

+10-2
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,15 @@ jobs:
2121
with:
2222
python-version: 3.8
2323

24+
- name: install elan
25+
run: |
26+
set -o pipefail
27+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
28+
./elan-init -y --default-toolchain none
29+
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
30+
2431
- name: lint
25-
continue-on-error: true
32+
continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions
2633
run: |
2734
./scripts/lint-style.sh --fix
2835
@@ -37,7 +44,7 @@ jobs:
3744
sudo apt-get install -y bibtool
3845
3946
- name: lint references.bib
40-
continue-on-error: true
47+
continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions
4148
run: |
4249
./scripts/lint-bib.sh
4350
@@ -65,6 +72,7 @@ jobs:
6572
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
6673
6774
- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
75+
continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions
6876
run: lake exe mk_all
6977

7078
- name: suggester / import list

0 commit comments

Comments
 (0)