Add rewrap checking to build (metamath#2416)

* Add rewrap checking to build

Unless I've misunderstood the discussion to date, we would prefer that
this be checked automatically so that we don't have a lot of "where do
these diffs come from? how are we supposed to prevent or fix them
again?" sorts of issues.

* Rewrap set.mm

* Do rewrapping on a temporary file

This might be just a cosmetic thing (the fact that I'm not
completely sure illustrates the point that mutation is hazardous) but
it seems better not to mutate set.mm and iset.mm themselves in the
rewrap check.

* Adjust scripts/rewrap order of operations

As suggested in CONTRIBUTING, run rewrap before save proof.

* Adjust CONTRIBUTING language about rewrapping

It is possible that most of the text introduced by "If you prefer
to run metamath yourself" can be removed or drastically pared
down, but at least for now maybe it is good to keep this for people who
are used to having it there? I don't think it is wrong per se.

.github/workflows/verifiers.yml

@@ -116,6 +116,16 @@ jobs:
       - run: scripts/regen-from-raw --force '/ALT_HTML' .regened.html
       - run: mkdir -p mpeuni-html/
       - run: for f in *.regened.html; do mv $f mpeuni-html/${f%.regened.html}.html ; done
+      # Check that set.mm and iset.mm have been rewrapped.
+      # We'd probably rather have a bot push up a commit with the rewrapping
+      # when a pull request is submitted, but until we set that up,
+      # at least check that the rewrapping has been done.
+      - run: cp set.mm set-wrapped.mm
+      - run: scripts/rewrap set-wrapped.mm
+      - run: echo 'Checking for set.mm rewrapping:' && diff -U 0 set.mm set-wrapped.mm
+      - run: cp iset.mm iset-wrapped.mm
+      - run: scripts/rewrap iset-wrapped.mm
+      - run: echo 'Checking for iset.mm rewrapping:' && diff -U 0 iset.mm iset-wrapped.mm
       # The following checks are arbitrarily included in the metamath job.
       - run: echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" set.mm
       - run: echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" iset.mm

CONTRIBUTING.md

@@ -58,12 +58,17 @@ is automatically licensed as such.
 
 ## Formatting recommendation prior to submitting a pull request
 
-Periodically we rewrap set.mm to help conform to its formatting conventions.
-This may affect your mathbox (your local sandbox)
-if you submitted it without rewrapping, possibly
-causing merge conflicts with your work in progress.
+On pull requests we check that set.mm and iset.mm have been rewrapped to
+help conform to their formatting conventions.
 
-Here is the procedure recommended prior to submitting a pull request:
+Locally you will need to run `scripts/rewrap set.mm` to avoid failing this
+check.
+
+If you prefer to run metamath yourself rather than via `scripts/rewrap`,
+the following commands should do the same thing, and/or help you detect
+other problems before submission. But if you want you can just leave it up to
+the automated verification checks and worry about rewrapping and the
+others if and when something fails.
 
 <PRE>
 ./metamath

scripts/rewrap

@@ -3,5 +3,8 @@
 # Rewrap source file $1 (default "set.mm")
 source="${1:-set.mm}"
 
-metamath "read ${source}" 'save proof */c/f' \
-  "write source ${source} /rewrap" quit
+# The reason for doing /rewrap first is so that 'save proof' will subsequently
+# adjust the proof indentation to match any indentation changes made by /rewrap.
+metamath "read ${source}" "write source ${source} /rewrap" \
+  'erase' "read ${source}" 'save proof */compressed/fast' \
+  "write source ${source}" quit