As I indicated on github, I support adding this CI check. The next metamath.exe version (0.199) fixes a minor /rewrap issue that affects 4 lines in set.mm, and these will annoyingly flip-flop back and forth in PRs until everyone updates to 0.199. So I think it makes sense to hold off releasing it until this CI check added. Any volunteers?
Norm On Saturday, November 6, 2021 at 10:05:09 AM UTC-4 Benoit wrote: > 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/67e0968b-46df-4310-8a1c-0abb8fddf05dn%40googlegroups.com.
