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/8fef813f-dc59-4438-8f45-2c75d83118a2n%40googlegroups.com.
