CONTRIBUTING.md: fix URLs, fix .md syntax, some rewrapping and minor rephrasing (#3603)

Author: benjub

CONTRIBUTING.md

@@ -18,12 +18,12 @@ meet those criteria when creating a contribution.
 
 First, take a look at some existing proofs.
 Walking through the
-[Metamath Proof Explorer (MPE, aka set.mm)](http://us.metamath.org/mpeuni/mmset.html) is a good way to start.
+[Metamath Proof Explorer (MPE, aka set.mm)](https://us.metamath.org/mpeuni/mmset.html) is a good way to start.
 
 To create a proof, you need to pick a tool.
 The Metamath system specifies a common file format, not a single tool
 everyone has to use.
-Many in the community use the [mmj2 tool](http://us.metamath.org#mmj2), and
+Many in the community use the [mmj2 tool](https://us.metamath.org#mmj2), and
 many of the rest use the original metamath C program (aka "metamath.exe").
 A third option is the [metamath-lamp tool](https://lamp-guide.metamath.org/),
 which can be accessed directly from your web browser at
@@ -39,7 +39,7 @@ to watch it, there's a video giving a
 You should start small and try to reprove what's already
 proven with Metamath before you try to prove something new.
 If you're contributing to set.mm or iset.mm, take a look at its
-[conventions and style](http://us.metamath.org/mpeuni/conventions.html).
+[conventions and style](https://us.metamath.org/mpeuni/conventions.html).
 
 At some point you should join the
 [Metamath mailing list](https://groups.google.com/g/metamath).
@@ -48,30 +48,28 @@ If you're seriously working on proofs, we'd love to help you get started!
 For contributing a final proof once you have one,
 you'll basically create a "pull request" on GitHub to request
 merging of some change(s) into the corresponding Git repository.
-**Warning**: Changes are made to the **develop** branch.
+**Warning:** Changes are made to the **develop** branch.
 The Wiki page
 [Getting started with contributing](https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing)
 will walk you through the process of contributing a final proof once you have one.
 
-**NOTE**: Any proposed contribution must be licensed under the
+**NOTE:** Any proposed contribution must be licensed under the
 [Creative Commons 0 (CC0) License](LICENSE), so any proposed contribution
 is automatically licensed as such.
 
 ## Formatting recommendation prior to submitting a pull request
 
-On pull requests we check that set.mm and iset.mm have been rewrapped to
-help conform to their formatting conventions.
+On pull requests, we check that `set.mm` and `iset.mm` have been rewrapped to
+help conform to their formatting conventions.  You may run the script
+`scripts/rewrap set.mm` to make sure your pull request passes this check.
 
-Locally you will need to run `scripts/rewrap set.mm` to avoid failing this
-check.
+If you prefer to run `metamath.exe` directly rather than via `scripts/rewrap`,
+the following commands should do the same thing, and/or help you detect other
+problems before submission.  If you want, you can just leave it up to the
+automated verification checks and worry about rewrapping and the other checks
+only if and when something fails.
 
-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>
+```bash
 ./metamath
 MM> read set.mm
 MM> write source set.mm /rewrap
@@ -82,149 +80,139 @@ MM> verify markup */file_skip/top_date_skip
 MM> verify proof *
 MM> write source set.mm
 MM> quit
-</PRE>
+```
 
 This can also be done as a single command in bash:
 
-<PRE>
+```bash
 ./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
-</PRE>
-
-or in one line, for ease of copypasting:
-
-<PRE>
-./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
-</PRE>
+```
 
-and for iset.mm:
+and for `iset.mm`:
 
-<PRE>
-./metamath 'read iset.mm' 'write source iset.mm /rewrap' erase 'read iset.mm' 'save proof */compressed/fast' 'verify markup */file_skip/top_date_skip' 'verify proof *' 'write source iset.mm' quit
-</PRE>
+```bash
+./metamath 'read iset.mm' 'write source iset.mm /rewrap' \
+   erase 'read iset.mm' 'save proof */compressed/fast' \
+   'verify markup */file_skip/top_date_skip' 'verify proof *' \
+   'write source iset.mm' 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.
-Then, 'verify markup' will check that no lines became too long due to different
-indentation.  Finally, 'verify proof' is there because you might as well.
+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`.  Then, `verify markup` will check that no lines became too long due
+to different indentation.  Finally, `verify proof` is there because you might
+as well.
 
 In addition, you are encouraged to run `scripts/minimize label`, where label is
 the name of your theorem. This script attempts to shorten the proof using other
 theorems in the database. Over many proofs, this can make a big difference in
 speeding up various functions, such as loading the database into a tool.
 However, this step is not a requirement for submissions to be accepted.
 
-(You can also check definitional soundness with mmj2 and any 'discouraged'
+You can also check definitional soundness with mmj2 and any "discouraged"
 markup changes before submission if you want, or you can just leave it up to
-the automated verification checks to check those.)
+the automated verification checks to check those.
 
 ## Regenerating the `discouraged` file
 
-In almost all cases, especially when you're starting, you won't need to
-regenerate the `discouraged` file. So if you're just starting out, you can
-probably ignore this section. However, there are rare cases when that
-is needed. This section explains what the discouraged file is all about.
+In almost all cases, especially when you are starting, you will not need to
+regenerate the `discouraged` file.  So if you are just starting out, you can
+probably ignore this section. However, there are rare cases when that is
+needed.  This section explains what the discouraged file is all about.
 
 Some statement descriptions in `set.mm` and `iset.mm` have one or both of the
-markup tags `(New usage is discouraged.)` and `(Proof modification is discouraged.)`.
-In order to monitor accidental violations of these tags in set.mm and iset.mm,
-we store the usage and proof lengths of statements with these tags in a file
-called `discouraged` for set.mm and `iset-discouraged` for iset.mm.
-The automated check will return an error if this file does not exactly match the
-one that it generates for a set.mm pull request.
+markup tags `(New usage is discouraged.)` and
+`(Proof modification is discouraged.)`.  In order to monitor accidental
+violations of these tags in `set.mm` and `iset.mm`, we store the usage and
+proof lengths of statements with these tags in a file called `discouraged` for
+`set.mm` and `iset-discouraged` for `iset.mm`.  The automated check will return
+an error if this file does not exactly match the one that it generates for a
+`set.mm` or `iset.mm` pull request.
 
 If you make modifications that affect the `discouraged` file, you should
 regenerate it with the following command under Linux or Cygwin bash:
 
-<PRE>
+```bash
 ./metamath 'read set.mm' 'set width 9999' 'show discouraged' quit \
     | tr -d '\015' | grep '^SHOW DISCOURAGED.' \
     | sed -E -e 's/^SHOW DISCOURAGED.  ?//' | LC_ALL=C sort > discouraged
-</PRE>
-
-or in one line, for ease of copypasting:
+```
 
-<PRE>
-./metamath 'read set.mm' 'set width 9999' 'show discouraged' quit | tr -d '\015' | grep '^SHOW DISCOURAGED.' | sed -E -e 's/^SHOW DISCOURAGED.  ?//' | LC_ALL=C sort > discouraged
-</PRE>
+and for `iset.mm`:
 
-and for iset.mm:
-
-<PRE>
-./metamath 'read iset.mm' 'set width 9999' 'show discouraged' quit | tr -d '\015' | grep '^SHOW DISCOURAGED.' | sed -E -e 's/^SHOW DISCOURAGED.  ?//' | LC_ALL=C sort > iset-discouraged
-</PRE>
+```bash
+./metamath 'read iset.mm' 'set width 9999' 'show discouraged' quit \
+    | tr -d '\015' | grep '^SHOW DISCOURAGED.' \
+    | sed -E -e 's/^SHOW DISCOURAGED.  ?//' | LC_ALL=C sort > iset-discouraged
+```
 
-The "tr -d '\015'" is needed with Cygwin to strip carriage returns and has no
-effect in Linux.
+The `tr -d '\015'` command is needed with Cygwin to strip carriage returns and
+has no effect in Linux.
 
 The `discouraged` file can also be regenerated with mmj2, which currently runs
-faster than metamath.exe for this function.
-See the automated verification script for the details.
-
+faster than `metamath.exe` for this function.  See the automated verification
+script for the details.
 
-The metamath.exe and mmj2 proof assistants will prevent most accidental
-violations.  The behavior of the metamath.exe proof assistant in the presence
+The `metamath.exe` and `mmj2` proof assistants will prevent most accidental
+violations.  The behavior of the `metamath.exe` proof assistant in the presence
 of these tags and how to override them is described in the 11-May-2016 entry of
-<http://us.metamath.org/mpeuni/mmnotes.txt>.
+<https://us.metamath.org/mpeuni/mmnotes.txt>.
 
 Please note that when you regenerate the `discouraged` file, before comitting
 it you should compare it to the existing one to make sure the differences are
-what you expected and there are no accidental changes elsewhere.
-The purpose of this file is to help detect such accidental changes, and if it
-is not inspected manually that purpose is defeated.
+what you expected and there are no accidental changes elsewhere.  The purpose
+of this file is to help detect such accidental changes, and if it is not
+inspected manually that purpose is defeated.
 
 ## What are the requirements for acceptance (merging)?
 
-A pull request (proposed change) *must* pass all verifiers before
-it will be merged (accepted). This even enforces some style rules on
-some databases, e.g., we want a name and date for each new theorem.
+A pull request (proposed change) *must* pass all verifiers before it will be
+merged (accepted).  This even enforces some style rules on some databases,
+e.g., we want a name and date for each new theorem.
 
 To be merged, a pull request must be approved by a different existing
-contributor (someone who's already had some previous contributions accepted).
-You can approve a change by viewing the pull request, selecting
-the tab "Files Changed", clicking on the "Review Changes" button,
-clicking on "Approve", and submitting the review.
-You can also approve by using the comment "+1".
-Feel free to approve something others have approved, that makes it clear
-there's no serious issue.
-
-*Note*: Reviewers should investigate a commit that changes a
-`discouraged` file, since this means the commit is doing something
-that is normally discouraged.  That doesn't make it wrong, it just means a
-rationale is needed.
-
-Once a pull request is approved (other than the person
-originally proposing the change), any maintainer can merge it,
-including the approver.
-A maintainer is a member or owner of the Metamath GitHub organization.
+contributor (someone who has already had some previous contributions accepted).
+You can approve a change by viewing the pull request, selecting the tab "Files
+Changed", clicking on the "Review Changes" button, clicking on "Approve", and
+submitting the review.  Feel free to approve something other contributors have
+already approved: that makes it clearer that there are no serious issues.
+
+**Note:** Reviewers should investigate a commit that changes a `discouraged`
+file, since modifying it means that the commit is doing something that is
+discouraged.  That does not make it wrong, it just means a rationale is needed.
+
+Once a pull request is approved (by someone other than the person originally
+proposing the change), any maintainer can merge it, including the approver.  A
+maintainer is a member or owner of the Metamath GitHub organization.
 
 We generally tend to have a bias towards "merge this now" with separate
-follow-up fixes for minor issues (e.g., to use a better name). That reduces the
-risk of losing good ideas, or a lot of rework, due to some minor
-blemish like an odd name. It's a pain to fix "merge conflicts"
-because differences have accumulated over time, and we'd rather avoid
-merge conflicts if there's no good reason to have them.
+follow-up fixes for minor issues (e.g., to use a better name).  That reduces
+the risk of losing good ideas, or a lot of rework, due to some minor blemish
+like an odd name.  It is a pain to fix "merge conflicts" because differences
+have accumulated over time, and we would rather avoid merge conflicts if
+there are no good reasons to have them.
 
-We encourage changes to be smaller, focusing on a single logical idea.
-That makes changes much easier to review.
-It also makes it easy to accept some changes while not accepting others.
+We encourage changes to be smaller, focusing on a single logical idea.  That
+makes changes much easier to review.  It also makes it easy to accept some
+changes while not accepting others.
 
 Many contributors have or create a personal "mathbox" - a sandbox of work that
-is visible to others. Changes to someone's own mathbox still go through a
-review, but usually it's cursory - we generally just want to ensure that those
-changes don't interfere with or confuse others.
-Mathbox changes must still pass all verifiers, though, and that is
-a very rigorous check.
-Mathboxes should normally only be changed by the owner of the
-mathbox (unless it's a general improvement that applies across the database).
-
-The following people are active and are willing to be contacted
-concerning the areas listed.  This area maintainership is not (at least
-currently) part of the approval/merge process described above, but hopefully
-this list will help you find people who work on a particular area.
-Please propose a change to this file if you want to be an area maintainer.
+is visible to others.  Changes to someone's own mathbox still go through a
+review, but usually it is cursory - we generally just want to ensure that those
+changes do not interfere with other parts of the database or confuse other
+contributors.  Mathbox changes must still pass all verifiers, though, and that
+is a very rigorous check.  Mathboxes should normally only be changed by the
+owner of the mathbox (unless it is a general improvement that applies across
+the database).
+
+The following people are active and are willing to be contacted concerning the
+areas listed.  This area maintainership is not (at least currently) part of the
+approval/merge process described above, but hopefully this list will help you
+find people who work on a particular area.  Please propose a change to this
+file if you want to be an area maintainer.
 
 * Mario Carneiro (@digama0): Any part of set.mm or iset.mm