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/20affe16-5248-44bc-ba0a-be0417594c6en%40googlegroups.com.
