As a general rule of thumb I think something that gets automatically checked when you submit a pull request is more contributor friendly than an unwritten rule (or even a rule which is written, but not enforced by a check).
I think maybe what we have now does the VERIFY MARKUP part but not the rewrap part? On November 4, 2021 1:10:53 PM PDT, 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. -- 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/B56CECDB-5DB1-4D67-B3A1-6E20A4338FFF%40panix.com.
