lint errors in mathlib PRs

Stream: general

[Emily Riehl]

I feel like I've been having a lot of trouble recently with unpredictable errors in my mathlib PRs that I don't understand. Maybe the issue is not actually something I have to worry about but every time I worry this is going to further delay an already very lengthy PR review process. What is the best practice for getting help when I can't figure it out myself?

The latest one is in PR #31101. The failure seems to have something to do with the lint style and conclude with

Run reviewdog/action-suggester@4747dbc9f9e37adba0943e681cc20db466642158
Run set -euo pipefail
🐶 Installing reviewdog ... https://github.com/reviewdog/reviewdog
  reviewdog/reviewdog info checking GitHub for tag 'v0.20.3'
  reviewdog/reviewdog info found version: 0.20.3 for v0.20.3/Linux/x86_64
  Error: Process completed with exit code 1.

[Bryan Gin-ge Chen]

I suspect the failure might be due to some issues that GitHub was having earlier today, cf. #mathlib4 > lake: command not found. I've retriggered the job using the "Re-run jobs" button on the log page, and now it's green.

[Chris Henson]

We had the exact same issue in CSLib today, also fixed by rerunning the job.

[Emily Riehl]

Thanks. I don't see exactly how you did that but I'll try and sort it out the next time something like this happens.

[Emily Riehl]

I have another immediate build failure that I think must be some issue with some job not running. Do I have the ability to rerun a job? If so, how?

[Ruben Van de Velde]

image.png
on https://github.com/leanprover-community/mathlib4/actions/runs/19583989117/job/56090581359?pr=31101

[Ruben Van de Velde]

The "re-run jobs" button on the right. But it seems to be a genuine error

[Ruben Van de Velde]

Error: error: Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean:338:8: Unknown identifier `h`

[Thomas Murrills]

You can also use this, depending on which tab you're on:
Untitled 3.jpg

[Ruben Van de Velde]

Note that github shows the "lint mathlib" section by default, while the error is in the "build mathlib" section

[Thomas Murrills]

(I think the "re-run all jobs" button in @Ruben Van de Velde's screenshot is in the "Summary" tab in the sidebar.)