In lean/mathlib, the solution used is to have a bot make and self-apply formatting PRs (well, actually it's more like updating the discouraged file but the concept applies to any automatic code change). I think this is friendlier for contributors than having a CI check flag your PR if it did not pre-apply the automatic change. (For linting and other indicators of bad code, it is better to keep the checks in the PR though, even if they can be automatically fixed, since we want such things to be flagged in review.)
On Thu, Nov 4, 2021 at 4:10 PM Glauco <[email protected]> wrote: > In the conversation for this pull request > > https://github.com/metamath/set.mm/pull/2285 > > there's been some discussion about adding a GitHub Action to check if the > submitted set.mm has the "recommended" format. > > > "Formatting recommendation prior to submitting a pull request" is > described here > > https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md > > The page also contains a one line bash command that should be run in order > to apply the recommended format. Here it is: > > ./metamath 'read set.mm' 'write source set.mm /rewrap' erase 'read set.mm' > 'save proof */compressed/fast' 'verify markup */file_skip/top_date_skip' > 'verify proof *' 'write source set.mm' quit > > > We are inclined to add a job that checks that this command was actually > launched, before the PR. Here's an example of what is now happening > (without the mandatory constraint): > - I do a PR where I add a couple hundred theorems and I forget to run the > command above > - today, the PR can be merged, and it is merged (sometimes, "somebody" > notices it was not properly formatted, and I am required to fix and commit; > but not in this example) > - later on, another contributor applies a few changes to set.mm and then, > as recommended, runs the above command, to get the standard formatting > - then she diffs with remote, and she gets a huge number of lines changed > (those from my previous PR) > > > Cons: this post > https://groups.google.com/u/1/g/metamath/c/1tDhd-VkYNE/m/Vrctk_fqAQAJ > is titled "Contributing is difficult." and I agree :-) > And maybe this would make it even more difficult. > > My opinion is that the reformatting back and forth we are exposed today, > should be prevented. > > Any comment? > > > BR > Glauco > > -- > 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/f8bb6d5e-6d99-46ad-9920-81ccb7cb72f9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f8bb6d5e-6d99-46ad-9920-81ccb7cb72f9n%40googlegroups.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/CAFXXJSt3KLeRbPCziSmwC%3DtfrD8oA04eYXxTaTwQk2%3DVyzW0Ng%40mail.gmail.com.
