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.
