Maybe "remove-braces" and "remove-dvs" ? You can probably do the PR and the discussion may continue there. Benoît
On Tuesday, November 2, 2021 at 4:37:30 AM UTC+1 [email protected] wrote: > 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/e04ea974-7051-4383-992c-618d18f2c21en%40googlegroups.com.
