Metavariable instantiation seems to slow down non-linearly in the size of the proof

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues

• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
  * This is rather hard, since the problem is one of scalability.

• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

  • Again, hard due to the lack of an MWE

Description

In (LNSym)[github.com/leanprover/LNSym] we produce quite large proofs, which seem to be bottlenecked by metavariable instantiation: in our most extreme benchmark, elaborating a theorem takes about 18 seconds in total, of which 10 seconds are spent in instantiateMVars.

Firstly, this time was not showing up in the trace.profiler output, but this is fixed in #5501.

The bigger question, is why is metavariable instantiation so slow?
Here's a table of some benchmarks we've run, with links to the source code and the resulting profile.

Benchmark	Profile	Elaboration Time (total)	instantiateMVars
SHA512_150	https://share.firefox.dev/4dsm3Is	3.9s	1.3s (34%)
SHA512_225	https://share.firefox.dev/4dsm3Is	6.9s	3s (44%)
SHA512_400	https://share.firefox.dev/4ev6y3E	17.7s	10s (56%)

To be clear: the instantiateMVars runtime reported in the table measures only the calls done in the MutualDef elaborator.

Context

To investigate the issue, we've experimented with a wrapper that remembers the goal metavariable at the start, runs the tactic, and then at the end reassigns the metavariable to it's instantiation (assuming that it's been assigned) --- see here for where the wrapper is used.

Surprisingly this had almost no effect on the time spent on metavariable instantiation in the elaborator code. The benchmarks table above use the commit which has this wrapper. To see the time taken, expand the tactic nodes until you see Tactic.sym: withInstantiatMainGoal.instantiateMVar and observe that even in the largest benchmark, instantiating mvars here takes only 5ms, as opposed to the 10 seconds spent in the elaborator.

Also, to be clear: these profiles were obtained by running Lean from the terminal, but running them in interactively in Lean gives roughly the same timings: this issue seems orthogonal from what's going on in #5614.

Steps to Reproduce

1. Clone LNSym
2. Checkout commit 8384b193b4c727da83b200f5132c7b4620d3b03d to get the experimental wrapper
3. Run make profiles to profile the benchmarks
4. You'll find the generated profile json files under data/profiles

If you're not running a toolchain with #5501 cherry-picked on it, you can deduce how much time is spent on instantiating mvars by looking at the self-time of the Elab.command node.

Expected behavior: I wouldn't expect the majority of elaboration time to be spent on instantiating mvars.

Actual behavior: The time spent on instantiating mvars seems to scale non-linearly with the size of the proof (or at least, it scales non-linearly with the time spent on evaluating the tactic that produced the proof), even if we force the tactic to fully instantiate it's original main goal.

Versions

nightly-2024-09-10, with #5501 cherry-picked on it (specifically, opencompl/fix-timeleak-nightly-2024-09-10)

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the LNSym SHA512_150, SHA512_225, and SHA512_400 benchmarks at the referenced commit, then run make profiles and inspect the generated files under data/profiles. Compare the instantiateMVars timings in the profiles with the MutualDef elaborator and the withInstantiatMainGoal.instantiateMVar tactic node. Done means identifying a reproducible cause of the scaling behavior and demonstrating improved benchmark timings.