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.

[Kim Morrison]

Could someone please work out how to disable reviewdog on PRs touching more than 300 files? Currently it just fails all such PRs with an error like:

         reviewdog: fail to get diff: GET https://api.github.com/repos/leanprover-community/mathlib4/pulls/11997: 406
         Sorry, the diff exceeded the maximum number of files (300).

[Kim Morrison]

I'm happy to make a PR disabling reviewdog in the meantime. :-)

[Alex J. Best]

cross posting from https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/.2311997.2C.20adaptations.20for.20nightly-2024-04-07/near/431907375 as likely many people are not subscribed over there (I wasn't)

The reviewdog set up was made with this sort of situation in mind to some extent, and I don't think it's necessary to disable reviewdog. The process is as follows: due to https://github.com/leanprover-community/mathlib4/blob/b8145adda2a744f3a646ee93f5daa05a4855da73/bors.toml bors should still merge even if review dog step fails, as long as the build steps work. Reviewdog will not run on draft PRs, so PRs where reviewdog failing is annoying (and we want a nice green tick) can be developed in draft mode, and then made non-draft and merged when ready to merge. Let me know if there is something I'm missing here (maybe the queue will ignore such PRs?).

[Ruben Van de Velde]

Does it actually block bors at this point, or just the overall :check: ?

[Alex J. Best]

I'm not sure what you are asking. If someone "bors merge"s a PR for which the reviewdog step fails then the merge should go through. Its just that the bottom of the PR will still have 1 "failed check" (also worth noting that reviewdog runs on PRs not commits so iirc these checks won't even be run on master)

[Ruben Van de Velde]

Right, that's what I meant. So failing reviewdog is more annoying than a blocker

[Kim Morrison]

Can we add a check that test if there are more than 300 files changed, and disables reviewdog in those cases. It's already hard enough to get a PR on the #queue, and it seems the workarounds above would prevent that?

[Alex J. Best]

Sure we can do that, I'm sure its not hard and chatgpt can likely write the invocation instantly for us. I will say that not being on #queue is probably not the reason 300 files changed PRs are not getting reviewed though, any such thing is likely accompanied by discussion here anyway.

[Kim Morrison]

Note that blocking the overall :check: messes with nightly-testing CI reporting.

[Kim Morrison]

@Alex J. Best, do you have time to disable reviewdog when more than 300 files have changed? I've disabled it entirely on nightly-testing for a while, but this is now getting in the way of getting adaptation PRs ready.

[Alex J. Best]

I took a look but I couldn't find a dead simple way to do this (i.e. an existing action), like probably it will take 30minutes to get something that works but I unfortunately dont have that time right now. There are already actions to print the list of changed files so it should just be a case of combining those with some bash scripting to make the job skip if that list is long

[Kim Morrison]

Okay, no problems, thanks for looking. I guess in the meantime I've got my adaptation PR down below 300 files, so all is well. :-)

[Eric Wieser]

Reviewdog made a total mess of a new contributor PR in https://github.com/leanprover-community/mathlib4/pull/11988

[Eric Wieser]

It looks like its whitespace suggestions somehow got caught in a race condition, and so it suggested a bunch of nonsensical changes that reverted to a previous revision

[Eric Wieser]

My general opinion is that lint_style.sh --fix is great, but reviewdog is on average noise and at worst super confusing. I think we could get just as much value by posting a comment telling the user to run lint_style.sh --fix, but maybe that command doesn't work on everyone's lean install...

[Kim Morrison]

Regarding reviewdog: it is meant to make a suggestion for when Mathlib.lean needs an update? I thought that was the case, but at #12058 it did not.

It would be good to know if this was never the case, or otherwise if something broke here.

[Kim Morrison]

(This PR was raised as a question in office hours, asking how to deal with the CI error, so clearly automatic assistance would have been useful!)

[Alex J. Best]

Reviewdog can only make suggestions on lines that the user changed, or those nearby, so unfortunately it can't suggest mathlib.lean updates most of the time. I don't know of any way around this and any suggestion based action will have the same problem.
It's been suggested elsewhere that having a bot that pushes the mathlib.lean update to the branch for you would be a better interaction mode in this case, and I'm inclined to agree. But bots that push to branches need to be a lot more bulletproof than those that just make suggestions

[Alex J. Best]

Idk about on average noise, I see it making many suggestions that users do apply. The main issues are with the mathlib.lean thing which has been around for long enough and nobody has been able to fix so maybe it's time to disable that part. Ofc it's behaviour is controlled by the linters themselves so if we have linters that are causing noise that's an independent problem.
In the case of 11988 I guess one of those unusual merge commits confused it which is unfortunate, maybe there is a bug there that needs investigating and reporting upstream?

[Alex J. Best]

@Kim Morrison it looks like your issue is already reported upstream https://github.com/reviewdog/reviewdog/issues/1696#issue-2206596164

[Johan Commelin]

My impression is also that reviewdog is actually quite useful, and in many cases the suggestions are applied. So I would be sad to see it go completely.

[Rida Hamadani]

Kim Morrison said:

(This PR was raised as a question in office hours, asking how to deal with the CI error, so clearly automatic assistance would have been useful!)

Since actions cannot suggest this change, I suggest at least adding the script/mk_all.sh command somewhere in the "how to contribute to mathlib" article.

[Rida Hamadani]

In case that sounds like a good idea, here is a small PR that does it.

[Kim Morrison]

We should definitely have the CI error message say that!

[Kim Morrison]

Rida Hamadani said:

In case that sounds like a good idea, here is a small PR that does it.

Thanks @Rida Hamadani, made a small suggestion, but yes, this is a good idea!

[Kim Morrison]

Merged!

[Yaël Dillies]

@Damiano Testa, we'll have to update the message once #11853 lands

[Moritz Firsching]

I'm also hitting the "the diff exceeded the maximum number of files (300)" thing in #12274

[Ruben Van de Velde]

Uhh.

[Ruben Van de Velde]

If you're going to do something like this, at the very least you should make sure that the big commits are completely autogenerated

[Jireh Loreaux]

I think we've been waiting to do this until we have a better ability to do global replacement.

[Moritz Firsching]

Ruben Van de Velde said:

If you're going to do something like this, at the very least you should make sure that the big commits are completely autogenerated

I split them up in a few commits, each starts with a regular expression replacement followed by a manual replacement where the replacement went wrong. I suppose I can make each one of those into two commits a big completely autogenerated one and a small one with manual fixes. That should make it easy to review.

[Moritz Firsching]

Jireh Loreaux said:

I think we've been waiting to do this until we have a better ability to do global replacement.

Ok, what the rationale behind this?

[Jireh Loreaux]

The existing refine' isn't doing much harm as is. And also, such a replacement would be a good test bed for a new global replacement tool.

[Jireh Loreaux]

And person-hours saved also.

[Moritz Firsching]

I have closed the pull request on the refine', if you think it is better to postpone it.
Nonetheless, while I was add it I looked into how to fix the "the diff exceeded the maximum number of files (300)" problem and #12280 contains a way to "fix" it, by disabling the reviewdog for pull request that touch more than 300 files. Of course an even better fix might be to find a way to run the reviewdog nonetheless, but I think this is something that would need to be fixed upstream at the reviewdog repo. Perhaps it is worth reporting this as a bug/feature-request there?

[Kim Morrison]

Alex noted above that there's already some discussion upstream at https://github.com/reviewdog/reviewdog/issues/1696#issue-2206596164.

[Moritz Firsching]

Cool, I will add a comment with a link to this discussion in the temporary fix

[Antoine Chambert-Loir]

Is it possible, either to apply all of the comments suggested by reviewdog, or to discard them all. I have hundreds of them because of trailing spaces and it is a nuisance to have to check them one by one on the website.

[Damiano Testa]

If it is just trailing spaces, this may fix them:

git ls-files '*.lean' | xargs sed -i 's=  *$=='

[Damiano Testa]

(I do not know if it is possible to accept in bulk all the suggestions by reviewdog.)

[Eric Wieser]

That shouldn't be necessary, you can just use lint-style.sh --fix

[Eric Wieser]

Which is what reviewdog is using to generate the suggestions anyway

[Eric Wieser]

That doesn't help with discarding the comments though

[Antoine Chambert-Loir]

So to discard the comments, the simplest seems to close the PR and to reopen another one?

[Eric Wieser]

Maybe this is an argument for not using reviewdog in the first place

[Antoine Chambert-Loir]

Do we have choice for that?

[Damiano Testa]

I do not find reviewdog terrible: most of the times, I am grateful that I can click a couple of suggestions to merge them and get CI to pass.

If it had a way of self-silencing when it would give more than some number of suggestions, that might be useful though.

[Damiano Testa]

I also remember that at some point, a PR touching over some number of files could not pass CI due to reviewdog. In that case, Alex manage to work around the issue.

[Alex J. Best]

@Antoine Chambert-Loir can you link to the pr in question so we can see how bad it looks. I would guess if you apply the linter on commandline and push all comments get marked as outdated already so hopefully aren't too distracting

[Antoine Chambert-Loir]

#9315

[Alex J. Best]

That pr was closed 7 months ago, is that really the right one?

[Damiano Testa]

#9359 maybe?

[Antoine Chambert-Loir]

Sorry, yes

[Alex J. Best]

I see, that PR looks ok on my device, I don't see loads of outdated comments or anything, so it sounds to me like applying on the command line was a good resolution and the most constructive thing we can do here is to add some reminders somewhere that reviewdog suggestions can be applied manually on your own device. Either in the reviewdog comment or on a contributing page on the website.

[Johan Commelin]

I think several users would be very happy if they can write a github comment @reviewdog fix this for me (or something like that). Would someone be willing to write a CI action for that?

[Michael Rothgang]

I like the idea! In terms of naming, @reviewdog fixsounds good. Perhaps reviewdog could mention this when posting comments, something like "Type @reviewdog fix in a comment to apply all unresolved suggestions."

[Johan Commelin]

The downside of @reviewdog <some fix message> is that it creates the illusion that reviewdog is involved in the fixing. So maybe it should just be something like

bot fix style

[Bryan Gin-ge Chen]

I took a quick look but it looks like I'll need to spend some time figuring out how reviewdog works before I can put a workflow together. If no one else wants to work on it I'll try to come back to this within a few days. I'd of course be happy to review a PR as well.

[Ruben Van de Velde]

I don't think you need to know anything about review dog, you just need to run the lint --fix command and push the results

[Eric Wieser]

This also means you need the dependencies of lint --fix installed, which used to include Python

[Bryan Gin-ge Chen]

Thanks, I think I can probably hack something together tonight then.

edit: something came up, but I should still be able to get to this before next week.

[Michael Rothgang]

Eric Wieser said:

This also means you need the dependencies of lint --fix installed, which used to include Python

It still does - the Python rewrite is not complete yet.

[Bryan Gin-ge Chen]

I've created a PR at #15781, but I haven't had a chance to test it out yet. I tried a few times to trigger the style linter and reviewdog by adding random spaces at the beginnings of lines in a leaf file but I couldn't get it to work (fail?). If someone wants to give it a shot please feel free!

edit: It looks like I may end up having to test this out in a fork, but still any commits to the branch would be appreciated!

[Johan Commelin]

Thanks for starting on this. I left a comment

[Bryan Gin-ge Chen]

This is finally ready for review. As I mention in the PR comment, you can test this out by going to my fork of mathlib4 and adding comments / PR reviews.

[Johan Commelin]

@Bryan Gin-ge Chen thanks for hacking on this. Atm it seems the github action isn't completely happy. But your experiments look like it did work in the past.

[Johan Commelin]

Or maybe I just ran into

For starters, if someone would like to try commenting bot fix style on bryangingechen#2 I can check if the permissions check is working properly. (Since no one other than me has write access at this time, hopefully the bot will ignore your comment.)

[Bryan Gin-ge Chen]

Yep, looks like it!
Screenshot-2024-08-26-at-06.17.11.png

I've given you write access now so you can test it further if you wish.

[Johan Commelin]

Just did another test

[Bryan Gin-ge Chen]

It failed again, but I checked the settings and it looks to me like you have to manually accept the invite for your permissions to change.

[Bryan Gin-ge Chen]

https://github.com/bryangingechen/mathlib4/invitations

[Johan Commelin]

good point, new attempt

[Johan Commelin]

The test seems to work

[Johan Commelin]

@Bryan Gin-ge Chen would you like to do more testing, or shall we merge your PR?

[Bryan Gin-ge Chen]

I've exhausted the tests that I could think of, so if everyone is happy with it we can merge. (I'm always afraid that there's something I've missed...)

[Johan Commelin]

Well, you aren't force pushing, so you can't do too much damage

[Johan Commelin]

[Bryan Gin-ge Chen]

Funny story, before I got the token set up properly, the first version of the script pushed to master instead of the PR branch...

[Kim Morrison]

Could we please:

1. Make sure the new token/secret usage is documented in the usual place.

[Kim Morrison]

2. Ideally use a new token and secret; ideally everything is only used in one place.

[Bryan Gin-ge Chen]

Thanks for the reminder, I'll try to do both tomorrow!

[Bryan Gin-ge Chen]

Done now, hopefully! #16232

[Bryan Gin-ge Chen]

It seems the new bot fix style command hasn't been used yet. I wonder if it's because people don't know it exists yet.

One thought would be to have the reviewdog action suggester mention it somewhere, but it seems the only thing we can customize is the tool name. So, where the suggestions currently say [lint-style] reported by reviewdog, we could make them say something like [lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] reported by reviewdog.

Thoughts?

[Johan Commelin]

Sounds like a good idea. It's a bit long though, but I don't have an immediate improvement in mind.

[Bryan Gin-ge Chen]

Thanks! I've opened #16365 for now.

[Johan Commelin]

I think reviewdog doesn't post suggestions for fixing Mathlib.lean (by running lake exe mk_all) or does it?
Can we easily add that functionality?

[Johan Commelin]

Because then bot fix style would also auto-fix those problems.

[Damiano Testa]

I think that it was intended that it did, but I also think that it doesn't.

[Yaël Dillies]

It definitely did for a long while. Doesn't seem like it does anymore

[Johan Commelin]

@Bryan Gin-ge Chen Do you by any chance know some back story here?

[Ruben Van de Velde]

I seem to recall that it made suggestions, but they were often wrong for some reason I never looked into

[Johan Commelin]

But lake exe mk_all should just do the right thing, shouldn't it?

[Johan Commelin]

I still wish we could just get rid of that CI step completely. And https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/generating.20Mathlib.2Elean/near/264350855 suggests that maybe we can.

[Johan Commelin]

I just want CI to create the file just before it runs the bors build on staging

[Damiano Testa]

The file could be not git-indexed and CI could generate it on the fly. However, having the option of import Mathlib is really good.

[Damiano Testa]

After all, CI already generates it on the fly and uses the one it generates for its checks.

[Johan Commelin]

Right. So why can't the autogenerated one be committed when bors decides that a batch gets merged.

[Damiano Testa]

I see no reason for this: you could have PRs with out-of-sync Mathli.lean, but CI nevertheless building everything and then in the final Bors staging commit the output of mk_all.

[Johan Commelin]

Yeah, that would be nice.

[Johan Commelin]

But atm I don't know how to do that. Because bors is a black box to me.

[Damiano Testa]

As it currently is, CI already pretends that you updated Mathlib.lean.

[Damiano Testa]

I've never looked at the staging CI, but presumably you can run some script before that could include mk_all?

[Johan Commelin]

I'm a bit worried that we hand over to bors before that point.

[Damiano Testa]

I'll have to look at the code, as Bors is a black box to me too.

[Damiano Testa]

It looks like bors merges the PRs and runs the "usual" CI. This probably means that some batches fail due to Mathlib.lean having failed to correctly (i.e. alphabetically) merge.

[Damiano Testa]

Would it be too aggressive to add a CI step that commits import changes if Mathlib.lean is out of sync?

[Johan Commelin]

If we can make bors reliably commit the correct mathlib.lean, then we also no longer need to bug users that the mathlib.lean in their PR is out of date.

[Johan Commelin]

Yeah, I would prefer if we do not need to commit to user PRs.

[Damiano Testa]

The staging script could do that, though?

[Damiano Testa]

After all, the staging script is generated to be virtually identical to CI, but we could have a different one instead.

[Johan Commelin]

I hope so. Where does that live? I have no idea which steps are part of the black box, and which parts we can tweak.

[Damiano Testa]

The CI script has a master file that is in .github/build....

[Damiano Testa]

That file auto-generates the remaining build scripts that are in .github/workflows.

[Johan Commelin]

Yes, but I didn't see anything about setting up staging. Maybe I didn't look carefully?

[Damiano Testa]

The one called bors.yml is the result of auto-generation, but auto-generation is run manually and has its own script mk_build_something.

[Damiano Testa]

I view all the CI steps in the bors.yml file as "pre-staging": there we may add a commit?

[Johan Commelin]

If we don't commit to user branches, but to a branch managed by CI / bors, that's totally fine.

[Yaël Dillies]

Johan Commelin said:

Yeah, I would prefer if we do not need to commit to user PRs.

But can we make it so that we don't have an extra "Update Mathlib.lean" commit on master for each bors batch?

[Damiano Testa]

It does not mean that bors receives a correct Mathlib.lean file, but it receives the same that it would now.

[Damiano Testa]

At worst, we can create a new PR with the extra commit and merge that.

[Damiano Testa]

So bors receives PR that already have a compliant Mathlib.lean

[Johan Commelin]

But then it merges the original branches, so we need to make sure that they have a compliant Mathlib.lean...

[Johan Commelin]

Johan Commelin said:

Yeah, I would prefer if we do not need to commit to user PRs.

Let me amend that a bit: I would really prefer if we do not commit to user branches, unless it is < 30 seconds before merging them.

[Johan Commelin]

So only between the point where bors decides " :check: yup we can merge this" and where bors actually carries out the merging.

[Damiano Testa]

Right, I'm thinking that instead of bors merge we do mk_all, commit, merge

[Johan Commelin]

commit on which branch?

[Johan Commelin]

bors merge can still fail...

[Damiano Testa]

Possibly the commit on a new branch that includes the modifications and the merge on that branch.

[Damiano Testa]

(Sorry, I'm on my phone and I'm about to see a student! I'll try to type something as soon as I'm in my office!)

[Damiano Testa]

How about

if lake exe mk_all
then
  bors merge
else
  git checkout -b new_branch
  git add -u
  git commit -m 'add imports'
  (create a PR)
  bors merge this PR
fi

(modulo a million extra safety checks)?

[Yaël Dillies]

What about

1. For each PR in the batch,
   a. Run lake exe mk_all on the branch
   b. Commit the result onto a new branch PR-N-staging where N is the PR number. Don't publish that branch
   c. Squash merge PR-N-staging onto staging (assuming no conflict). If there is a conflict in Mathlib.lean, fix it by running lake exe mk_all again.

2. Run CI on staging

3. If CI passes, rebase master on staging

[Yaël Dillies]

Pros:

• No need to bother about lake exe mk_all whil making a PR
• No extra commit on master
• Each commit corresponds to the content of the relevant PR

[Johan Commelin]

Sounds totally fine, but once again, I don't know where to implement your steps.

[Yaël Dillies]

I think it's in bors' guts

[Jireh Loreaux]

It would be very strange to hardcode lake references inside bors, even if it is our own fork.

[Johan Commelin]

We could hardcode functionality to run a pre-bors-hook and a post-bors-hook.