search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.57k stars 405 forks source link

RFC: in TC resolution, `← instantiateMVars (← inferType mvar)` is computed 2 or 3 times over for every new goal #4284

Closed JovanGerb closed 1 month ago

JovanGerb commented 4 months ago

Proposal

These three lines do this same computation:

https://github.com/leanprover/lean4/blob/f05a82799a01569edeb5e2594cd7d56282320f9e/src/Lean/Meta/SynthInstance.lean#L286 https://github.com/leanprover/lean4/blob/f05a82799a01569edeb5e2594cd7d56282320f9e/src/Lean/Meta/SynthInstance.lean#L243 https://github.com/leanprover/lean4/blob/f05a82799a01569edeb5e2594cd7d56282320f9e/src/Lean/Meta/SynthInstance.lean#L474

I propose to do it once, and pass this result as an argument to all these functions.

kim-em commented 4 months ago

Is there evidence that this change by itself would have a performance impact?

JovanGerb commented 4 months ago

I hadn't tested it separately yet, but here's a PR for it now: #4379 Fixing only this also involved moving the withMCtx around a bit, because the instantiateMVars needs to be in the relevant metavariable context. I have an issue for this here #4286

JovanGerb commented 4 months ago

The result of the test on Mathlib is that this change is responsible for all of the performance improvement in #4277.