fix: ensure instantiateMVarsProfiling adds a trace node

[alexkeizer]

We add a new Meta.instantiateMVars trace node to the instantiateMVarsProfiling definition used in elabMutualDef, and we replace various uses of plain instantiateMVars with the profiled version (which necessitated pulling up the definition to be higher in the file).

This fixes a "time leak" when profiling large proofs, where instantiating the goal metavariable can take a significant amount of time, that previously would not be accounted for when using the trace profiler.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56b78a0ed104c896c033bcd2284449cea2dd5d12 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 21:52:40)

[hargoniX]

!bench to ensure the code doesn't introduce non trivial regressions.

[hargoniX]

I'm also not exactly sure that this is the proper solution for the instantiateMVars time leak. This is only going to profile it in very specific situations, a more uniform solution seems more desirable to me? But also potentially more threatening to performance.

[leanprover-bot]

Here are the benchmark results for commit e78addd.
There were significant changes against commit 56b78a0:

  Benchmark                 Metric       Change
  =======================================================
+ import Lean               task-clock   -11.4% (-12.9 σ)
+ import Lean               wall-clock   -11.5% (-12.9 σ)
+ lake config tree          task-clock    -9.3% (-17.4 σ)
+ lake config tree          wall-clock    -9.3% (-16.7 σ)
+ language server startup   task-clock    -1.8% (-13.6 σ)
+ language server startup   wall-clock    -1.8% (-10.4 σ)

[alexkeizer]

I'm also not exactly sure that this is the proper solution for the instantiateMVars time leak. This is only going to profile it in very specific situations, a more uniform solution seems more desirable to me? But also potentially more threatening to performance.

Fair point. It should be noted that instantiateMVarsProfiling was already a thing, I just expanded its use and ensured it has a trace node so that it shows up in the trace profiler also, previously it would only show up in the other profiler.

The proper solution would be to add a trace node to instantiateMVars itself, I agree, but that is a lot trickier. Lean.Util.Trace (which defines the trace machinery) imports Lean.MetavarContext (where instantiateMVars lives), so we'd have to figure out why this is, and I suspect we'd have to split MetavarContext up.