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.
