I agree with Glauco and Alexender about adding an automatic check in the CI, since merge conflicts can be particularly annoying. And copypasting a line from https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md is not that difficult.
I also agree with Jim that checking is better than silently rewriting a submission, which could cause confusion. Benoît On Saturday, November 6, 2021 at 10:10:35 AM UTC+1 Alexander van der Vekens wrote: > 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/1cdc3bca-4d83-43df-ad65-3b518c4adc21n%40googlegroups.com.
