Support for Lean language build errors #21
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Vierkantor
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 23, 2025
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
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 24, 2025
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
tannerduve
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 13, 2025
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a file with support for Lean error message syntax.
We use the
problem-matcher-wrapaction in CI for projects in the Lean language, especially https://github.com/leanprover-community/mathlib4. Lean changed its error message syntax a while back, and so the nice error messages stopped appearing. With the newleanproblem matcher regex added in this PR, everything should work again with the latest versions of Lean.Example of the annotated output:
(Screenshots from https://github.com/leanprover-community/mathlib4/actions/runs/14617507898/job/41009027153).