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/ebd26153-a736-46a8-9729-f75bdf506a34n%40googlegroups.com.
