File: CONTRIBUTING.md

package info (click to toggle)
metamath-databases 0.0.0~20210101.git55fe226-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm, bullseye, sid
  • size: 48,584 kB
  • sloc: makefile: 7; sh: 6
file content (109 lines) | stat: -rw-r--r-- 4,447 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
If you are new to GitHub and git, the basic instructions for
contributing changes to set.mm are described in the wiki,
[Getting started with contributing](https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing).
(Feel free to enhance the wiki.)

The rest of this note shows how to achieve the recommended
formatting for set.mm and iset.mm prior to submitting your changes.

### 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 if you submitted it without rewrapping, possibly
causing merge conflicts with your work in progress.

Here is the procedure recommended prior to submitting a pull request:

<PRE>
./metamath
MM> read set.mm
MM> write source set.mm /rewrap
MM> erase
MM> read set.mm
MM> save proof */compressed/fast
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>
./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:

<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>

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.

(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
Travis to check those.)


### Regenerating the `discouraged` file

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 Travis check will return an error if this file does not exactly match the
one that it generates for a set.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>
./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:

<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>

The "tr -d '\015'" 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 Travis 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
of these tags and how to override them is described in the 11-May-2016 entry of
http://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.