Both methods worked. Thanks ! What do you plan to do with these 245 pairs in set.mm (around 100 of them in Main). Remove them manually to check we do not remove intentional structuring ? This could be a collective work (I could take e.g. 50), and should be coordinated to avoid merge conflicts with other PRs. Same questions with extra DVs.
Can you do a PR to add both scripts to set.mm/scripts ? Benoît On Sunday, October 31, 2021 at 5:15:30 PM UTC+1 [email protected] wrote: > Try running it like this: > > awk -f metamath-braces set.mm > > If you prefer to run it as a command, then make sure it has the executable > bits set: > > chmod 0755 metamath-braces > > Then either place it in some directory in your $PATH, or explicitly give > the directory where it is located, e.g.: > > ./metamath-braces set.mm > > On Sunday, October 31, 2021 at 10:04:58 AM UTC-6 Benoit wrote: > >> I have trouble running the awk script. Can you see what is wrong ? >> >> $ sh metamath-braces set.mm >> metamath-braces: 24: BEGIN: not found >> metamath-braces: 25: /${: not found >> metamath-braces: 26: /${/: not found >> metamath-braces: 27: Syntax error: "(" unexpected >> [and using bash, basically the same thing happens] >> $ bash metamath-braces set.mm >> metamath-braces: ligne 24: BEGIN : commande introuvable >> metamath-braces: ligne 25: /${: Aucun fichier ou dossier de ce type >> metamath-braces: ligne 26: /${/: Aucun fichier ou dossier de ce type >> metamath-braces: ligne 27: erreur de syntaxe près du symbole inattendu « >> ( » >> metamath-braces: ligne 27: `/\$\}/ { if (empty[i] != 0) print(empty[i]); >> delete empty[i] }' >> $ metamath-braces set.mm >> bash: metamath-braces : commande introuvable >> $ uname -r >> 5.10.0-9-amd64 >> >> >> On Sunday, October 31, 2021 at 4:34:04 PM UTC+1 [email protected] wrote: >> >>> If I change the script to not ignore braces containing only comments, >>> then it triggers on comments about the braces, such as on line 12383 of >>> set.mm (as of today). I've worked on both scripts and made the >>> following changes. >>> >>> The metamath-braces script now reports the line number of the opening ${ >>> instead of the name of the final theorem in the block. That seems more >>> useful. I've taken a different approach to skipping over instances of "${ >>> ... }$" in the comments, and it seems to work. Braces containing only >>> comments are now reported. >>> >>> The metamath-dvs.py script now records the variables mentioned in $e >>> statements, and counts those as uses when examining $d statements. This >>> fixes the bug Thierry Arnoux pointed out. >>> >>> The new versions are available at the same URLs as before: >>> http://jamezone.org/pleasure/mathematics/metamath-braces >>> http://jamezone.org/pleasure/mathematics/metamath-dvs.py >>> >>> On Saturday, October 30, 2021 at 5:09:00 AM UTC-6 Benoit wrote: >>> >>>> 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/26849558-d68c-4ec6-8214-8ad738e440a0n%40googlegroups.com.
