perf: skip re-attempting pending TC mvars with unchanged instantiated goals (quadratic resumption, #14448)#14449
Open
grandchildrice wants to merge 1 commit into
Open
Conversation
…ntheticMVars The resumption loop re-attempts every pending `.typeClass` synthetic metavariable whenever any single one makes progress. In statements whose literals/operators create a chain of interdependent default-instance mvars (each assignment unlocks the next), k pending instances cost k+(k-1)+... = O(k^2) synthInstance attempts, each an expensive underdetermined (mvar-headed) search. Microbench (200 theorems `7 + ... + 7 = 7 + ... + 7`, k per side, term-mode rfl), per-command elaboration cost on master (25ba8c3): 1.64 / 3.22 / 8.43 / 27.6 / 101.4 ms for k = 1/2/4/8/16 (x3.3-3.7 per doubling => quadratic). Controls: the same expressions in defs (known expected type) and theorems over variables are both linear. Fix: memoize per pending mvar the instantiated goal type at its last failed attempt (one MVarIdMap Expr in Term.State); skip the re-attempt when the instantiated goal is unchanged. synthInstance is deterministic in the instantiated goal for a fixed env/local-instance context, so the skip elides only attempts whose outcome is already known. With the fix the k=16 case drops ~4.7x and oleans are byte-identical. Gated behind `Elab.tcSkipUnchanged` (default false) for evaluation.
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes the quadratic re-attempt behavior described in #14448.
Elab.synthesizeSyntheticMVars' resumption loop re-attempts every pending.typeClasssynthetic metavariable whenever any single one makes progress; chained literal statements resolve one mvar per pass, giving O(k²) underdeterminedsynthInstanceattempts per command (~101 ms/command at 16 chained literals on master, quadratic scaling ×3.3–3.7 per doubling; see the issue for the full series and linear controls).Change: memoize per pending
.typeClassmvar the instantiated goal type at its last failed attempt (Term.State.tcSynthAttempt : MVarIdMap Expr); skip the re-attempt when the instantiated goal is unchanged.synthInstanceis deterministic in the instantiated goal for a fixed env/local-instance context, so the skip elides only attempts whose outcome is already known — pending mvars stay pending, and resolution happens exactly when the goal actually changes.Gated behind
Elab.tcSkipUnchanged(default false) so it can be evaluated safely; intended to become default-on if accepted (happy to drop the option or flip the default per maintainer preference).Evidence (this branch, on top of 25ba8c3):
Batteries.Data.List.Lemmas); real numeral-dense Mathlib module (NumberTheory.PythagoreanTriples) −7.4 % wall; isolated-literal modules neutral (win is specific to the chained-literal regime)