Mandatory "standard" formatting prior to submitting a pull request?

[Glauco]

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

[Mario Carneiro]

In lean/mathlib, the solution used is to have a bot make and self-apply formatting PRs (well, actually it's more like updating the discouraged file but the concept applies to any automatic code change). I think this is friendlier for contributors than having a CI check flag your PR if it did not pre-apply the automatic change. (For linting and other indicators of bad code, it is better to keep the checks in the PR though, even if they can be automatically fixed, since we want such things to be flagged in review.)

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f8bb6d5e-6d99-46ad-9920-81ccb7cb72f9n%40googlegroups.com.

[Jim Kingdon]

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?

[Glauco]

I think maybe what we have now does the VERIFY MARKUP part but not the rewrap part?

Yes, what we have now is a job that checks the VERIFY MARKUP part

[Alexander van der Vekens]

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.

[Benoit]

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

[Norman Megill]

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