Zulip Chat Archive

Stream: mathlib4

Topic: nolint workflow failed

Michael Rothgang (Apr 15 2025 at 15:31):

The latest "update nolints" workflow failed: https://github.com/leanprover-community/mathlib4/actions/runs/14424502470/job/40451294006. #23914 and #23868 were the last PRs to modify the workflow. @Anne Baanen @Bryan Gin-ge Chen (as the PR's author/main reviewer) in case one of you wants to look into CI fires, here's a small one. Not critical, but useful eventually :-)

Anne Baanen (Apr 15 2025 at 15:57):

Seems I forgot to move the "print Lean version" after the step that actually installs Lean. I won't be at a computer tonight, so feel free to steal this work from me :)

Michael Rothgang (Apr 15 2025 at 16:03):

#24088

Anne Baanen (Apr 15 2025 at 16:28):

Looks good to me, thanks! And sorry for the silly mistake.

Bryan Gin-ge Chen (Apr 15 2025 at 16:39):

If I remember correctly lean-action prints the lake and lean version too so we could even remove that step if we wanted. (I think the PR is fine as is though!)

Michael Rothgang (Apr 15 2025 at 21:24):

Removing that step would be an excellent follow-up. Who would like to file the PR? :-)

Last updated: May 02 2025 at 03:31 UTC