I endorse the suggestion to automatically check if the submitted set.mm has the "recommended" format before a PR is accepted. It increase quality and avoids unnecessary discusions/merge conflicts. For a beginner it may be some extra effort, but she/he will learn it quickly, and then gain profit of the quality.
On Thursday, November 4, 2021 at 9:10:53 PM UTC+1 Glauco 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/71e88ad1-0ff3-489f-8d69-04bd94f99d5an%40googlegroups.com.
