Opening a pull request would be great, in the case of my mathbox. On November 30, 2021 7:44:11 PM PST, 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.
-- 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/C99A06B7-8AD8-4AC6-8C0F-F662D13A1A22%40panix.com.
