You wrote "ignore braces that do not include any $p statements". Maybe make it "ignore braces that do not include any $p statements nor any $a-statements" ? Or even, don't ignore them ? Is there a reason to keep braces enclosing only comments ?
Thanks for the clarifications. Benoît On Saturday, October 30, 2021 at 1:04:36 AM UTC+2 [email protected] wrote: > For the first point, the ${ $} pair can enclose more than one > $-statement. Specifically, once a ${ is seen, the script starts watching > for any of $c, $d, $e, $f, or $v. (That's the last line of the awk > script.) If it sees the matching $} without finding any, then it reports > that pair of braces. I made it ignore braces that do not include any $p > statements (the next to last line) because there are some used solely to > contain comments. > > For the second point, yes there might still be extraneous dv conditions. > Finding those would take significantly more work. Also note that Thierry > Arnoux found a bug in that script. I will try to fix it this weekend. > > On Friday, October 29, 2021 at 4:49:03 AM UTC-6 Benoit wrote: > >> Nice ! Just to clarify: >> >> The first script finds ${--$} pairs which enclose at most one (or exactly >> one?) $-statement, and that $-statement is a $p-statement (what if the >> single $-statement is an $a-statement ? the awk program does not seem to >> take them into accound). >> >> As for the second: it removes $d conditions among non-occurring variables >> (whether in the statement or in the proof, i.e., dummy variables). But >> there could still remain extraneous dv conditions. Correct ? Would it be >> doable to find these as well ? >> >> Thanks, >> Benoît >> >> >> On Friday, October 29, 2021 at 8:11:28 AM UTC+2 Thierry Arnoux wrote: >> >>> Hi Jerry, >>> >>> Very nice! >>> >>> I think we shall remove those unnecessary braces, and the "braces" >>> script could be added to our continuous integration, checking at every >>> commit that no new useless braces are added. >>> At least we shall add the "braces" script to metamath's script directory. >>> >>> Concerning the distinct variable statements however, I think you have >>> some false positives. It for example detects `.x.` at line 728127, that is >>> for theorem ~lincresunit2 in AV's mathbox. When I remove this DV, MMJ2 >>> complains it's missing. `.x.` actually appears in the essential hypothesis >>> ~lincresunit.t. There are other examples, it seems to be when the essential >>> hypothesis actually appears before the DV declaration. >>> Otherwise you seem to have done a good job avoiding the pitfall of >>> variables which are introduced in the proof, but don't appear either in the >>> theorem statement, nor in the essential hypothesis. Those have to be >>> declared as distinct variables anyway. There was a discussion thread about >>> removing those, but I think we decided to keep them for the moment. >>> >>> BR, >>> _ >>> Thierry >>> >>> >>> On 29/10/2021 11:17, 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/ff2c85a4-8ddd-4b6b-b27a-bf5867addf81n%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/ff2c85a4-8ddd-4b6b-b27a-bf5867addf81n%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/51e2fac1-151d-414f-aab6-2738a74cfb10n%40googlegroups.com.
