Skip to content

Commit 1afbc43

Browse files
VierkantorVierkantor
committed
fix(CI): use Lean error message in problem-matcher-wrap (#24316)
This PR fixes the missing build error message annotations in GitHub. Lean switched to a different syntax for error messages, and the action we used to annotate the commit/PR with those errors did not have support for that format. I made a fork of the action that does know how to parse Lean error messages, and use that to wrap the builds. For example, see the output of [this build](https://github.com/leanprover-community/mathlib4/actions/runs/14617507898/job/41009027153): <img width="1078" alt="Screenshot 2025-04-23 at 13 26 32" src="https://github.com/user-attachments/assets/944da832-6089-43e4-a7cf-9e073f18c79e" /> <img width="1162" alt="Screenshot 2025-04-23 at 14 07 16" src="https://github.com/user-attachments/assets/26aebffc-ea32-45ed-8f07-b3f0e1cad4de" /> I also opened [a PR to the original repo](liskin/gh-problem-matcher-wrap#21). If that gets merged, we can switch back to the upstream repo for this action. We do not need to change the format for linter/shake steps: those still fit the previous GCC-compatible syntax. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/gh-problem-matcher-wrap Fixes: #12946
1 parent 5e62daf commit 1afbc43

File tree

6 files changed

+28
-28
lines changed

6 files changed

+28
-28
lines changed

‎.github/build.in.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -157,9 +157,9 @@ jobs:
157157
158158
- name: build mathlib
159159
id: build
160-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
160+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
161161
with:
162-
linters: gcc
162+
linters: lean
163163
run: |
164164
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
165165
@@ -277,23 +277,23 @@ jobs:
277277
278278
- name: test mathlib
279279
id: test
280-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
280+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
281281
with:
282-
linters: gcc
282+
linters: lean
283283
run:
284284
lake --iofail test
285285

286286
- name: check for unused imports
287287
id: shake
288-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
288+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
289289
with:
290290
linters: gcc
291291
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
292292

293293
- name: lint mathlib
294294
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
295295
id: lint
296-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
296+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
297297
with:
298298
linters: gcc
299299
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib

‎.github/workflows/bors.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -167,9 +167,9 @@ jobs:
167167
168168
- name: build mathlib
169169
id: build
170-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
170+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
171171
with:
172-
linters: gcc
172+
linters: lean
173173
run: |
174174
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
175175
@@ -287,23 +287,23 @@ jobs:
287287
288288
- name: test mathlib
289289
id: test
290-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
290+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
291291
with:
292-
linters: gcc
292+
linters: lean
293293
run:
294294
lake --iofail test
295295

296296
- name: check for unused imports
297297
id: shake
298-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
298+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
299299
with:
300300
linters: gcc
301301
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
302302

303303
- name: lint mathlib
304304
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
305305
id: lint
306-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
306+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
307307
with:
308308
linters: gcc
309309
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib

‎.github/workflows/build.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -174,9 +174,9 @@ jobs:
174174
175175
- name: build mathlib
176176
id: build
177-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
177+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
178178
with:
179-
linters: gcc
179+
linters: lean
180180
run: |
181181
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
182182
@@ -294,23 +294,23 @@ jobs:
294294
295295
- name: test mathlib
296296
id: test
297-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
297+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
298298
with:
299-
linters: gcc
299+
linters: lean
300300
run:
301301
lake --iofail test
302302

303303
- name: check for unused imports
304304
id: shake
305-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
305+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
306306
with:
307307
linters: gcc
308308
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
309309

310310
- name: lint mathlib
311311
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
312312
id: lint
313-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
313+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
314314
with:
315315
linters: gcc
316316
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib

‎.github/workflows/build_fork.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -171,9 +171,9 @@ jobs:
171171
172172
- name: build mathlib
173173
id: build
174-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
174+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
175175
with:
176-
linters: gcc
176+
linters: lean
177177
run: |
178178
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
179179
@@ -291,23 +291,23 @@ jobs:
291291
292292
- name: test mathlib
293293
id: test
294-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
294+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
295295
with:
296-
linters: gcc
296+
linters: lean
297297
run:
298298
lake --iofail test
299299

300300
- name: check for unused imports
301301
id: shake
302-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
302+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
303303
with:
304304
linters: gcc
305305
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
306306

307307
- name: lint mathlib
308308
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
309309
id: lint
310-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
310+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
311311
with:
312312
linters: gcc
313313
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib

‎.github/workflows/latest_import.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,9 +57,9 @@ jobs:
5757
5858
- name: build mathlib
5959
id: build
60-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
60+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
6161
with:
62-
linters: gcc
62+
linters: lean
6363
run: |
6464
lake build
6565

‎.github/workflows/nolints.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,9 +41,9 @@ jobs:
4141

4242
- name: build mathlib
4343
id: build
44-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
44+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
4545
with:
46-
linters: gcc
46+
linters: lean
4747
run: |
4848
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
4949

0 commit comments

Comments
 (0)