leanprover
perf: deduplicate work in `isDefEq`
On a unification goal of the form f a₁ ... aₙ =?= f b₁ ... bₙ, the function tryHeuristic is sometimes called twice. If the expressions contains metavariables, then the permanent cache cannot be used, and this leads do a duplication (and potentially exponential increase) of work in isDefEq when the two expressions do not unify.
I solve it by changing the return type from MetaM LBool to MetaM (Except Bool Bool), where the Bool exception tells whether the function tryHeuristic has already been tried.
I identified this problem when working on #4592, where it caused a maxHeartbeats error.
The overall speedup of mathlib is 0.1%, with the following two major speedups:
Benchmark Metric Change
==========================================================================
+ ~Mathlib.Data.Finset.Pointwise instructions -15.7%
+ ~Mathlib.Probability.Kernel.Disintegration.Density instructions -19.0%
Hmmm, the Mathlib CI isn't happening automatically?
My bad. Once https://github.com/leanprover/lean4/pull/4632 is merged your next push might have chance of doing the mathlib thing again.
@JovanGerb, I think this is too little payoff for the requisite work to review and vet this.
A 0.1% speedup on all of Mathlib is below the noise threshold. Neither of the affected files are particularly large or slow. (Moreover, one is more or less a leaf in Mathlib.)
To justify the review work and correspondence required to get the PR into shape, we'd want to see evidence of greater I'm impact.
That's okay, I was hoping for a more significant speedup as well.
But I think 0.1% is above the noise threshold for instuctions for Mathlib as a whole (from what I've seen the the random fluctuations are always at most ±0.01%). It's just for single files that the fluctuations can be much bigger.