RFC: Only use a ReplaceExpr cache above a certain size

While doing some further measurements with valgrind's DHAT on std4 (the reason I'm sticking to std4 is that valgrinding mathlib4 files just takes an eternity) I noticed that in basically all files a significant chunk (read up to 40%) of the memory allocated during the life time of the compiler process is consumed by the ReplaceImpl Cache datastructure (https://github.com/leanprover/lean4/blob/master/src/Lean/Util/ReplaceExpr.lean#L19) , so I decided to take a look.

I made the Cache.new function print the size of the caches it creates, here is a bar chart of size vs count, measured over a full run of lake build on std4:

As we can see the majority of these caches are allocated for very small expressions which doesn't only cause us to spend quite some amount in the allocator to obtain basically trivial amounts of memory but at the same time makes it rather unlikely we are going to see a high hit rate for the caches. This is also confirmed by DHAT measurements which commonly report close to the same amount of reads and writes per byte in the memory allocated for Cache on many of files that get compiled in std4.

I thus propose we only allocate caches/use cached replacement for non trivial expression sizes. This does of course open up the question of what "non trivial expression sizes" are. In my demo implementation of this feature in #2510 I decided to set this threshold to an estimate depth of 5, this comes down to a cut-off at 31 in the above bar chart so right at the last big peak. I didn't measure this on all of std4 yet but in the files that I tested it did cause significant drops in instruction count and allocated memory. I believe this is because the replace implementation is most notably getting called during invocations of inferType which are of course all over the place.

It could of course be, that there are cases in the wild with very small expressions that do end up benefiting so much from the caching that this change is not worth it but I would hope that further benchmarks on the compiler and mathlib can provide an answer to this (and ideally rule it out ;)).

Start with src/Lean/Util/ReplaceExpr.lean and inspect ReplaceImpl.Cache.new and its callers. Review the measurements from std4, reproduce the lake build and DHAT benchmarks, and compare the demo implementation in pull request #2510. Done means agreeing on a cache-size threshold and showing the change improves compiler memory or instruction counts without meaningful regressions on std4 and mathlib.