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.
On 1/2/22 9:07 PM, Mario Carneiro wrote:
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]
<mailto:[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
<https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md>
file with the following text: "On pull requests we check that
set.mm <http://set.mm> and iset.mm <http://iset.mm> have been
rewrapped to help conform to their formatting conventions. Locally
you will need to run |scripts/rewrap set.mm <http://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
<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]
<mailto:[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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSusK3mqzMH6beCdNSzmuOEQU-Nt9sdquFS%3DnfC123tD2w%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSusK3mqzMH6beCdNSzmuOEQU-Nt9sdquFS%3DnfC123tD2w%40mail.gmail.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/58557dea-45f2-fb35-8655-f1cb10cb0c47%40panix.com.
