scripts/rewrap-comments.py: rewrap comments without a metamath build - #5456
vince-gonzalez wants to merge 4 commits into
Conversation
scripts/rewrap runs "write source /rewrap" through metamath, which also runs "save proof */compressed/fast" and reindents proof bodies. A change that touches comments and not proofs needs only the comment filling, and this does that part in Python with the standard library. The rules are transcribed from rewrapComment() in mmpars.c and the line-breaking loop of printLongLine() in mminou.c. Comments it does not model are left untouched and named: those containing <HTML>, those not attached to a $a or $p, and twelve across set.mm and iset.mm where a ~ reference and a long URL make a run that cannot be broken. Checked against metamath 0.199.pre. Running "write source /rewrap" on set.mm and iset.mm and comparing every statement comment gives 50578 and 17188 in agreement and none in disagreement. The reference leaves the comments of both databases unchanged, so both are in rewrapped state. Run over the databases in this repository the output is byte-identical to the input for set.mm, iset.mm, hol.mm, nf.mm, ql.mm, miu.mm, demo0.mm and big-unifier.mm. peano.mm differs on five comments; it contains "set.mm. We" and "peano.mm. They", one space where rewrap always writes two.
Review by @wlammen on metamath#5456. An inclusion may sit between a comment and the statement it describes. metamath resolves inclusions before parsing, so the statement test now skips over any "$[ ... $]" rather than reading "$[" as a label. None of the databases in this repository use inclusions, so nothing here changes; without this a comment followed by an inclusion was left alone.
|
(linking #2381) |
…xecutable wlammen's review: a deviation from the metamath executable's behavior belongs in the header even when no database in this repository triggers it, and the bare word "metamath" reads ambiguously where the executable is meant.
|
@wlammen do you think we can merge this PR ? |
|
I am not sure. The COMMENT expression is NOT a valid regular expression identifying comments. The reason is that two $$ are a replacement for a single literal $ in the comment text. It should not combine with a closing parenthesis. So I'm not that familiar with Python to easily investigate problems like this. The code comments should explain how the program handles exceptional cases like this. |
$) is a whitespace-delimited keyword and the language has no $$ escape (mmpars.c readRawSource; the deliberately-removed $$ case), so the first $) is always the comment terminator. Noted in review of metamath#5456.
|
The first The language has no So ending at the first Added a comment on the regex noting this (368e9f2). |
|
The basic version of the syntax is written in 4.1.2 and 4.1.3 of the Metamath book. And that is in fact in support of your view that no $$ token exists. Let me post some general observations around the software development of Metamath in general. It was seen as an advantage to have multiple implementation of verifiers and tools available. So if one was deficient, the others would soon detect the error. This is certainly true, and enhances the trust in set.mm contents. I see several topics where an improvement could help in the future:
Your proposal belongs to the third item in this list. You want to isolate the wrapping process currently bundled with other features. Fine, as for the basic idea, but it adds to the problems mentioned in the items and paragraphs before. This is just my personal view. Others may think differently. Metamath is a project that has to be maintained in a team. |
| help="name the comments left alone even when none changed") | ||
| args = ap.parse_args() | ||
|
|
||
| with open(args.database, encoding="utf-8", errors="replace") as f: |
There was a problem hiding this comment.
I would question whether errors="replace" is appropriate.
Your script is modifying the source file. If set.mm is supposed to be valid UTF-8, silently changing an invalid byte into � could corrupt the file, before writing it back.
| start = text.rfind("\n", 0, m.start()) + 1 | ||
| prefix = text[start:m.start()] | ||
| block = m.group(0) | ||
| following = text[m.end():m.end() + 160] |
There was a problem hiding this comment.
You look at the following 160 characters to find a statement. What is this constant based on? Is it possible to have more than 1 comment in front of a statement label?
| # a comment not attached to a statement is never reflowed by the | ||
| # metamath executable. | ||
| return False | ||
| budget = width - indent - 3 |
There was a problem hiding this comment.
You need to look at line 187 to understand the 3 (?)
| return "".join(NB if tmpl[p] == NB else c[p] for p in range(n)) | ||
|
|
||
|
|
||
| def normalize(comment): |
There was a problem hiding this comment.
What is the intended semantics of normalize? Comment missing
|
Thanks — that's the right citation, better than my paraphrase. The maintenance point is the real one. This is a second implementation of the wrap rules, and a second implementation can drift. What keeps it honest is that it doesn't have to be trusted on its own — its output either matches "write source /rewrap" or it doesn't, and on current develop it matches on all 56,054 comments. Run that diff in CI and the redundancy becomes the cross-check you called the strength of having several tools, not the drift you're wary of; the executable stays the source of truth, this just lets a contributor fix wrapping without building it first (the #2381 barrier). That's the whole aim — nothing to merge over a reservation. Fine to let it sit for the team. Thanks for looking again under load. |
4 participants
CONTRIBUTING asks for
scripts/rewrapbefore a PR, and that shells out to the C program. Obtaining it is enough of a step that the repo carriesscripts/download-metamathandscripts/build-metamath, and CI runs the download as its own job. @david-a-wheeler mentioned on #5448 wanting to distribute a cosmopolitan build partly for this.This does the comment-filling half in Python, standard library only. CC0 per CONTRIBUTING.
Scope
write source /rewrapis followed bysave proof */compressed/fast, which reindents proof bodies. This script does not touch proofs, so a proof change still needs the binary. A comment change leaves the proofs alone andsave proofdoes nothing, which is the case this covers.Comments it does not model are returned untouched and their labels printed: 123 containing
<HTML>, which metamath skips as well, anything not attached to a$aor$p, and 12 across set.mm and iset.mm where a~reference and a long URL make a run that cannot be broken.Verification
The rules are transcribed from
rewrapComment()inmmpars.cand the break loop inprintLongLine()rather than inferred from the corpus. That is the argument; the corpus is how the transcription gets checked.Run over every database in the repo, output is byte-identical to input for
set.mm,iset.mm,hol.mm,nf.mm,ql.mm,miu.mm,demo0.mmandbig-unifier.mm.peano.mmdiffers on 5 comments — it containsset.mm. Weandpeano.mm. They, one space where rewrap always writes two, so I take it to be not in rewrapped state.Each of the 67,742 comments accepted in
set.mmandiset.mmwas then damaged six ways — unwrapped onto one line, re-wrapped at 55 and at 70 columns, sentence gaps collapsed, extra spaces inserted, and a line broken between~and its label — and required to come back byte-identical. That is 325,517 cases whose correct output is already in the file, and all of them return it.Checked against metamath 0.199.pre itself:
write source /rewraponset.mmandiset.mm, then comparing every statement comment. 50,578 and 17,188 in agreement, none in disagreement. The reference also leaves both databases' comments unchanged, confirming they are in rewrapped state.