perf: reduce allocations in unused variable linter

[hargoniX]

Unlike #2471 I do have a reason and two data points that actually back this one up! I measured the most memory allocating functions using valgrind's DHAT tool while running a recent lean nightly on std4's biggest file (Std/Data/List/Lemmas.lean). The DHAT viewer shows that (among other things) this forEachExprWhere call is responsible for a significant chunk of allocations:

The initial count of total allocations was (a second run yielded almost identical numbers):

==3641472== Total:     2,524,478,041 bytes in 964,045 blocks

Judging from the doc-string in the implementation of forEachExprWhere it should only be favored over forEachExpr if the proposition (in this case isFVar) doesn't hold for many subterms. However there are of course a ton of subterms that are free variables here. So I decided to try and switch this to forEachExpr instead which yielded:

==3644111== Total:     1,750,132,393 bytes in 952,715 blocks

on the same file, the allocation chunk also disappeared from my measurements. I furthermore measured std4 compilation time and did get a measurable speedup in:
before:

lake build  369.35s user 14.23s system 446% cpu 1:25.95 total

after:

lake +lean4 build  288.33s user 12.46s system 436% cpu 1:08.92 total

I thus again request someone with privileges to give the bench run a try^^

[kim-em]

• ✅ Mathlib branch lean-pr-testing-2491 has successfully built against this PR. (2023-08-31 05:27:37)

[kim-em]

Here are the bench results from Mathlib: http://speed.lean-fro.org/mathlib4/compare/93695581-e592-41ad-9a6a-53fe2cce9e75/to/5b225066-90b6-4cd2-94f1-9aabc1be69ef. Seems okay, saves 0.6% wall-clock, essentially all from linting.

[digama0]

Scott, did you use your personal API key for the bot again? That's really confusing!

[kim-em]

Scott, did you use your personal API key for the bot again? That's really confusing!

Yes, but only while I'm testing. I put in the requests for the correct keys before I told the bot my token for today. :-)

[Kha]

Nice analysis. We should point this out in the forEachExprWhere docstring as well, not just the module docstring. But that can go into a different PR.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 20aa03c.
There were no significant changes against commit f7bff16.

[tydeu]

@Kha, I wonder why linting did not show as a significant change? The change is well above the 10 standard deviations (it's 85.6 stddev) and 1% threshold (it's 12.8%) in the formula.