Two cleanliness scripts

[Jerry James]

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/

[Thierry Arnoux]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ff2c85a4-8ddd-4b6b-b27a-bf5867addf81n%40googlegroups.com.

[Benoit]

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

[Jerry James]

That's an interesting bug.  I'll have to do a little code work this weekend to see if I can fix that.  Thanks for catching it.  And thank you for the kind words.

[Jerry James]

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.

[Benoit]

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

[Jerry James]

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

[Benoit]

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

[Jerry James]

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

[Benoit]

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

[Jerry James]

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.

[Benoit]

Maybe "remove-braces" and "remove-dvs" ?  You can probably do the PR and the discussion may continue there.

Benoît

[Jerry James]

Okay.  The pull request is here: https://github.com/metamath/set.mm/pull/2289

[Jerry James]

Once https://github.com/metamath/set.mm/pull/2335 is merged, the only remaining dv conditions on unused variables will be in mathboxes in set.mm.  I'm a little nervous about opening pull requests for others' mathboxes.  I would hate to cause a merge conflict for someone in the midst of working on the mathbox.  I can send you a patch for your mathbox, open a pull request in your behalf, or ignore the issue, as you wish.  I have patches for the following mathboxes:

- Thierry Arnoux

- Jonathan Ben-Naim

- Mario Carneiro

- Scott Fenton

- Jeff Hankins

- Jeff Hoffman

- Jim Kingdon

- ML

- Brendan Leahy

- Jeff Madsen

- Giovanni Mascellani

- Norm Megill

- Stefan O'Rear

- Jon Pennant

- Richard Penner

- Stanislas Polu

- Steve Rodriguez

- Andrew Salmon

- Alan Sare

- Glauco Siliprandi

- Alexander van der Vekens

- Emmett Weisz

[Mario Carneiro]

I would suggest erring in the other direction here: Except for currently-active contributors who object within some time horizon, I think you should just go ahead and make these edits to the mathboxes. Maintenance changes at this level have been done many times in the past, and there is no way you are going to get positive confirmation from many contributors, who may have moved on to other things (and at least one contributor has already passed away). People coming back after a long absence will have to acclimate to many changes to set.mm in any case.

Feel free to make a PR for my mathbox.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fcb62f8c-ecac-42b0-b2b1-b3eebfb95059n%40googlegroups.com.

[Jim Kingdon]

Opening a pull request would be great, in the case of my mathbox.

[Alexander van der Vekens]

It's fine for me if you clean up my mathbox.

Alexander

[Thierry Arnoux]

No problem for me either, you can go ahead and update my Mathbox.

Le 1 déc. 2021 à 12:34, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> a écrit :



It's fine for me if you clean up my mathbox.

Alexander

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/08500d13-564b-436f-b955-fbf0b2b684b8n%40googlegroups.com.

[Stanislas Polu]

Same here.

-stan

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/42E8D556-4355-4A0C-8CEC-344552DE4275%40gmx.net.

[Norman Megill]

You can update my mathbox.  However, this is clearly a maintenance edit, and in principle no permission is needed  per http://us.metamath.org/mpeuni/mathbox.html: "other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors."  I guess we could add to that, "removing redundant disjoint variable conditions" to be explicit.

For maintenance changes like this affecting many mathboxes, it should be sufficient to announce either here or as a GitHub issue that in say a week you will be making the changes if there are no objections, rather than waiting for every mathbox owner to respond.

Norm

[Glauco]

No problem for my mathbox

Glauco

[Jerry James]

Okay.  Since the consensus seems to be to go ahead, here is the pull request: https://github.com/metamath/set.mm/pull/2339.  That's the last one.  After that is merged, all of the mm files will be free of dv conditions on unused variables.

[Jerry James]

I just opened a pull request for the second part of this: removing unnecessary curly braces.  See https://github.com/metamath/set.mm/pull/2365.  If anybody wants me to keep my hands off of your mathbox, please let me know.  That should mark the end of the cleanup for now.  Regards,

On Thursday, October 28, 2021 at 9:17:21 PM UTC-6 Jerry James wrote: