Pull requests now check for rewrapping

[Jim Kingdon]

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.

[Mario Carneiro]

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).

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/35fb2a49-f338-c025-1cdc-3e88a197ce76%40panix.com.

[Jim Kingdon]

I think we're all agreed that a bot would be better (although I now see there would be more than one way to write it). I'm not trying to discourage anyone from making a bot happen at all.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSusK3mqzMH6beCdNSzmuOEQU-Nt9sdquFS%3DnfC123tD2w%40mail.gmail.com.

[Benoit]

On Monday, January 3, 2022 at 7:21:20 AM UTC+1 kin...@panix.com wrote:

I think we're all agreed that a bot would be better (although I now see there would be more than one way to write it). I'm not trying to discourage anyone from making a bot happen at all.

I agree with Jim and Mario.  I view the current CI check as a temporary solution before the solution described by Mario is implemented.  The discussion can be continued at https://github.com/metamath/set.mm/issues/2381

Benoît