-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: ensure instantiateMVarsProfiling
adds a trace node
#5501
base: master
Are you sure you want to change the base?
Conversation
This fixes a "time leak" when profiling large proofs, where instantiating the goal meta variable can take a significant amount of time.
instantiateMVarsProfiling
adds a trace node.instantiateMVarsProfiling
adds a trace node
Mathlib CI status (docs):
|
!bench to ensure the code doesn't introduce non trivial regressions. |
I'm also not exactly sure that this is the proper solution for the |
Here are the benchmark results for commit e78addd. 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 σ) |
Fair point. It should be noted that The proper solution would be to add a trace node to |
We add a new
Meta.instantiateMVars
trace node to theinstantiateMVarsProfiling
definition used inelabMutualDef
, and we replace various uses of plaininstantiateMVars
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.