I would suggest erring in the other direction here: Except for currently-active contributors who object within some time horizon, I think you should just go ahead and make these edits to the mathboxes. Maintenance changes at this level have been done many times in the past, and there is no way you are going to get positive confirmation from many contributors, who may have moved on to other things (and at least one contributor has already passed away). People coming back after a long absence will have to acclimate to many changes to set.mm in any case.
Feel free to make a PR for my mathbox. On Tue, Nov 30, 2021 at 10:44 PM Jerry James <[email protected]> wrote: > Once https://github.com/metamath/set.mm/pull/2335 is merged, the only > remaining dv conditions on unused variables will be in mathboxes in set.mm. > I'm a little nervous about opening pull requests for others' mathboxes. I > would hate to cause a merge conflict for someone in the midst of working on > the mathbox. I can send you a patch for your mathbox, open a pull request > in your behalf, or ignore the issue, as you wish. I have patches for the > following mathboxes: > > - Thierry Arnoux > - Jonathan Ben-Naim > - Mario Carneiro > - Scott Fenton > - Jeff Hankins > - Jeff Hoffman > - Jim Kingdon > - ML > - Brendan Leahy > - Jeff Madsen > - Giovanni Mascellani > - Norm Megill > - Stefan O'Rear > - Jon Pennant > - Richard Penner > - Stanislas Polu > - Steve Rodriguez > - Andrew Salmon > - Alan Sare > - Glauco Siliprandi > - Alexander van der Vekens > - Emmett Weisz > > On Thursday, October 28, 2021 at 9:17:21 PM UTC-6 Jerry James wrote: > >> I have been studying parts of set.mm that I want to understand better. >> While doing so, I have occasionally encountered unnecessary ${ $} pairs, >> and occasionally have seen $d statements for variables that do not appear >> in the theorems or proofs in that scope. Tonight I wrote a pair of scripts >> to detect these situations. It is a testament to the simplicity of the >> metamath grammar that I could write both in a single evening. >> >> Here is a 5-line awk script that identifies unnecessary braces: >> http://jamezone.org/pleasure/mathematics/metamath-braces >> >> This is the number of unnecessary brace pairs per mm file (skipping those >> with zero): >> - iset.mm: 51 >> - nf.mm: 56 >> - set.mm: 207 >> >> For the second issue, I started writing awk code as well, but quickly >> came to the realization that the line-oriented nature of awk was not well >> suited to the task. Here is a python script that finds $d statements for >> variables that do not appear below the $d in the same scope: >> http://jamezone.org/pleasure/mathematics/metamath-dvs.py >> >> This is the number of variables it found per file (skipping those with >> zero): >> - hol.mm: 1 >> - iset.mm: 1302 >> - nf.mm: 390 >> - set.mm: 6124 >> >> Unnecessary braces and $d statements are not critical issues, of course. >> I offer these scripts to anyone who wants to declutter a metamath database. >> >> Regards, >> -- >> Jerry James >> http://jamezone.org/ >> > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/fcb62f8c-ecac-42b0-b2b1-b3eebfb95059n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/fcb62f8c-ecac-42b0-b2b1-b3eebfb95059n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsyJG_43jyMxcKQsL12_JZ2wJpTJvRdkdQ731%2BEbXwVsg%40mail.gmail.com.
