Yes, I think they should be removed manually. I'm still not 100% certain those scripts are working as intended, so it would be good to have a human look at each one.
Sure, I can add those scripts to set.mm/scripts. What do you think of the names? The "metamath-" prefixes seem redundant. On Sunday, October 31, 2021 at 10:55:19 AM UTC-6 Benoit wrote: > 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/fcbc8b50-c8d4-4551-ba47-5121957ac67an%40googlegroups.com.
