reviewdog

Stream: mathlib4

[Bolton Bailey]

On #6428 commit 0e6a004, I get a CI failure with the following message:

Run reviewdog/action-suggester@v1
Run set -euo pipefail
🐶 Installing reviewdog ... https://github.com/reviewdog/reviewdog
Run set -euo pipefail
📖 reviewdog -h
Run set -euo pipefail
No local changes to save
reviewdog: GET https://api.github.com/repos/leanprover-community/mathlib4/pulls/6428/comments?per_page=100: 500  []
Error: Process completed with exit code 1.

What is reviewdog/what does this mean?

[Ruben Van de Velde]

Reviewdog is supposed to add suggestions on the pr to fix linter errors

[Johan Commelin]

cc @Alex J. Best

[Bolton Bailey]

Ruben Van de Velde said:

Reviewdog is supposed to add suggestions on the pr to fix linter errors

That's awesome! For more context, I eventually got another error telling me I was missing a docstring for a def. Is reviewdog supposed to recommend anything in that case?

[Ruben Van de Velde]

AI isn't that smart yet - it's more for things where there's a simple and obvious fix

[Alex J. Best]

No it won't recommend anything in this case indeed.
Sorry for the trouble! I'll make another pr to fail more gracefully and another couple of tweaks (maybe skipping wip prs also or changing the rate somehow would help, I see the bot has been annoying @Joël Riou regarding #4197 also). I'll also try and understand why that failed that time but looking at the error code seems quite inscrutable.

[Bolton Bailey]

A couple more questions.

1. Is there an example of a type of error that currently triggers reviewdog?
2. Why haven't I seen any reviewdog comments on my own PRs?
3. Can we program our own reviewdog triggers?

[Alex J. Best]

1. Currently only the style linter triggers it (plus the check all imports in mathlib.lean and the bibfile linters).
2. If it has anything to say it should say it I believe, so maybe you just haven't made the type of errors it knows how to autofix (You can see instances of it at work by searching in https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+reviewdog). Maybe very old PRs also have to merge master for it to start working im not sure?
3. Yes you can modify how it works for all of mathlib fairly easily, the whole thing is based off of the automated linter fixes added in #6568, this is a python script that reads in all the lines of lean files, looks at them and then outputs what it thinks the line should be, this can be used to add autofixes that, remove lines, modify them or add new lines entirely fairly easily. Unfortunately these scripts do not yet talk to lean itself so are limited at the moment to only fixing issues that could be seen from the source alone. I'd like it in the future if lean could also recommend such fixes via the same mechanism but a bit more work is needed to get that running

[Yaël Dillies]

Are you sure it is working correctly? #7605

[Bolton Bailey]

Seems it's telling you how to fix the extra whitespace you have that is unneeded and being caught by the linter?

[Bolton Bailey]

Hmm, is it saying it wants to delete the line?

[Alex J. Best]

Does it also complain on the command line?

[Bolton Bailey]

The corresponding line in the linter https://github.com/leanprover-community/mathlib4/blob/3f4910debcdd03d6ca9f9063b698a36fd2e3c211/scripts/lint-style.py#L160

[Alex J. Best]

Maybe we can also have reviewdog display which linter failed? That would be easier to interpret.
Are you saying that the PR had a windows line ending Bolton?

[Bolton Bailey]

No, it had trailing whitespace. You can see the error by going to the linter output https://github.com/leanprover-community/mathlib4/actions/runs/6465820999/job/17552670437

[Bolton Bailey]

And if you look at the raw file, indeed there was a space on line 471

[Bolton Bailey]

Looking at the linter I can't see any reason why it would be deleting the line rather than just removing the whitespace. I'm tempted to think this is just how GitHub displays that change.

[Bolton Bailey]

I'd be interested to see what happens if someone were to try applying the change

[Bolton Bailey]

Unfortunately for my curiosity it's already been fixed here though. Let me try another PR

[Bolton Bailey]

More concerning is that reviewdog keeps skipping the job I think this has to do with the not-tagged for review status, this makes sense.

[Bolton Bailey]

Ok I got it to work

[Bolton Bailey]

https://github.com/leanprover-community/mathlib4/pull/7172
Seems that this is just how GitHub writes it, mystery solved

[Bolton Bailey]

It's weird, I would have expected it to show a red - for deleting the line with the space and a green + for adding the line without the space.

[Ruben Van de Velde]

Yeah, I've noticed that when suggesting such changes manually on github as well

[Bolton Bailey]

I had the bright idea of writing a linter to break the lines too long errors in #7580. Reviewdog went a little hard after I started using the Github review function to make the changes, resuggesting all the other changes.

[Ruben Van de Velde]

Oops. I think "Add suggestion to batch" might have helped

[Bolton Bailey]

Does reviewdog allow doing that automatically?

[Alex J. Best]

There should always be the option yes, if its greyed out you can hover over it in the github UI to see why, iirc maybe you have to be in the "files" tab to batch things

[Bolton Bailey]

What are the conditions needed to get reviewdog to make suggestions? I was hoping to get a big list of suggestions on my linter PR #7496 but CI has run and no suggestions.

[Bolton Bailey]

Does it need to be marked awaiting-review?

[Bolton Bailey]

Is reviewdog unwilling to make over 150 suggestions at a time perhaps?

[Ruben Van de Velde]

Oh huh, this is an issue with our CI configuration. lint_and_suggest_pr.yml (which runs reviewdog) seems to be triggered only when you create a PR, while the style linter that runs when you push to a branch is triggered from build.yml, which doesn't run reviewdog

[Bolton Bailey]

I forked off a new PR #7795 but I still get no reviewdog

[Moritz Firsching]

I think the reviewdog is only looking at files (or even on lines) changed in your pr?
I had the same thing happening here: #7283

[Alex J. Best]

You can locally run ./scripts/lint-style.sh --fix though

[Alex J. Best]

That said I'm not sure these would be super useful suggestions for reviewdog, if this simply replaces simp by simp? but we have no suggester to replace things with the output of Try this for simp? then the user will have to open the files in Lean then anyway so the benefit of having reviewdog make the change suggestions on the PR is a bit limited

[Alex J. Best]

I think there is benefit for new users who dont know about simp? still, but probably not for most mathlibers

[Bolton Bailey]

Yeah the optimal would be for it to actually replace with the "Try This" output (and have that always work). A downside is that suggestions can clog up the PR page. Still, making a simp -> simp? suggestion seems slightly better to me than not doing so, because I no longer have to hunt through the file for the error, it gets highlighted in blue this way.