Okay. The pull request is here: https://github.com/metamath/set.mm/pull/2289
On Tuesday, November 2, 2021 at 3:03:24 PM UTC-6 Benoit wrote: > 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/64d30b74-cd81-4c04-b0d7-26d2cc6120d2n%40googlegroups.com.
