Skip to content

Commit 6304f2e

Browse files
VierkantorVierkantor
committed
fix(CI): use Lean error message in problem-matcher-wrap
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. 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 942869b commit 6304f2e

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
@@ -168,9 +168,9 @@ jobs:
168168
169169
- name: build mathlib
170170
id: build
171-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
171+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
172172
with:
173-
linters: gcc
173+
linters: lean
174174
run: |
175175
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
176176
@@ -288,23 +288,23 @@ jobs:
288288
289289
- name: test mathlib
290290
id: test
291-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
291+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
292292
with:
293-
linters: gcc
293+
linters: lean
294294
run:
295295
lake --iofail test
296296

297297
- name: check for unused imports
298298
id: shake
299-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
299+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
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@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
307+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
308308
with:
309309
linters: gcc
310310
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
@@ -178,9 +178,9 @@ jobs:
178178
179179
- name: build mathlib
180180
id: build
181-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
181+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
182182
with:
183-
linters: gcc
183+
linters: lean
184184
run: |
185185
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
186186
@@ -298,23 +298,23 @@ jobs:
298298
299299
- name: test mathlib
300300
id: test
301-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
301+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
302302
with:
303-
linters: gcc
303+
linters: lean
304304
run:
305305
lake --iofail test
306306

307307
- name: check for unused imports
308308
id: shake
309-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
309+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
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@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
317+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
318318
with:
319319
linters: gcc
320320
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
@@ -185,9 +185,9 @@ jobs:
185185
186186
- name: build mathlib
187187
id: build
188-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
188+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
189189
with:
190-
linters: gcc
190+
linters: lean
191191
run: |
192192
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
193193
@@ -305,23 +305,23 @@ jobs:
305305
306306
- name: test mathlib
307307
id: test
308-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
308+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
309309
with:
310-
linters: gcc
310+
linters: lean
311311
run:
312312
lake --iofail test
313313

314314
- name: check for unused imports
315315
id: shake
316-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
316+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
317317
with:
318318
linters: gcc
319319
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
320320

321321
- name: lint mathlib
322322
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
323323
id: lint
324-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
324+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
325325
with:
326326
linters: gcc
327327
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
@@ -182,9 +182,9 @@ jobs:
182182
183183
- name: build mathlib
184184
id: build
185-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
185+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
186186
with:
187-
linters: gcc
187+
linters: lean
188188
run: |
189189
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
190190
@@ -302,23 +302,23 @@ jobs:
302302
303303
- name: test mathlib
304304
id: test
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:
307-
linters: gcc
307+
linters: lean
308308
run:
309309
lake --iofail test
310310

311311
- name: check for unused imports
312312
id: shake
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 shake --gh-style
317317

318318
- name: lint mathlib
319319
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
320320
id: lint
321-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
321+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
322322
with:
323323
linters: gcc
324324
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
@@ -68,9 +68,9 @@ jobs:
6868
6969
- name: build mathlib
7070
id: build
71-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
71+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
7272
with:
73-
linters: gcc
73+
linters: lean
7474
run: |
7575
lake build
7676

‎.github/workflows/nolints.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,9 @@ jobs:
4646
4747
- name: build mathlib
4848
id: build
49-
uses: liskin/gh-problem-matcher-wrap@e7b7beaaafa52524748b31a381160759d68d61fb # v3.0.0
49+
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
5050
with:
51-
linters: gcc
51+
linters: lean
5252
run: |
5353
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
5454

0 commit comments

Comments
 (0)