Although checking for rewrapping in CI works, it has the side effect that e.g. drive-by review suggestions generally break the PR, and will probably result in lots of rewrap commits on the part of the PR author, which I think is a suboptimal situation. Instead, we can not check rewrapping at all in PR commits and have a bot follow up every commit to master with a rewrap commit, so that PR authors and reviewers are not bothered but we also don't have the cleanup issue.
I think the main reason this isn't being done is "who writes the bot", but if scripts/rewrap already exists then it should be as simple as a CI job triggering on master commits that calls scripts/rewrap and commits the result (with a bot credential, this requires some setup but it's not too hard last I checked). On Sun, Jan 2, 2022 at 3:22 PM Jim Kingdon <[email protected]> wrote: > Probably most people who have contributed to metamath have noticed the way > that our rewrapping scripts and practices tend to lead to things like > generating diffs in your pull request which are unrelated to the change you > are making (because the last person didn't rewrap and you did, typically). > > After some consultation between Benoit, Mario and me (and maybe others in > the past), we have changed the github checks so that a pull request must > have run rewrap into order to pass the automated checks. If your pull > request fails this check, you just need to run scripts/rewrap and push the > results, which should fix the failure. > > I've updated the > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md file with > the following text: "On pull requests we check that set.mm and iset.mm > have been rewrapped to help conform to their formatting conventions. > Locally you will need to run scripts/rewrap set.mm to avoid failing this > check." Although the commands which had been listed there are still > perfectly fine, my intention is that the only thing you need to worry about > is scripts/rewrap. I'm hoping that among other things this will be easier > for new contributors, who just have to deal with "how do I fix this failing > build?" and not "here are some rules which are written but not enforced and > if you don't do it that's OK but others will kind of wonder what happened > and maybe it is only sort of OK" which is roughly the situation we have > been in, as I see it. > > If there are any questions or concerns, just ask (for example, here or on > https://github.com/metamath/set.mm/issues/2381 ). We can always change > this again if people don't like it, I can help explain how it now works, > etc. > > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/35fb2a49-f338-c025-1cdc-3e88a197ce76%40panix.com > <https://groups.google.com/d/msgid/metamath/35fb2a49-f338-c025-1cdc-3e88a197ce76%40panix.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSusK3mqzMH6beCdNSzmuOEQU-Nt9sdquFS%3DnfC123tD2w%40mail.gmail.com.
