From 916004bd3cddce36a930df49579c16838b23281e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 31 Mar 2026 21:27:15 +0200 Subject: [PATCH] fix: add checkSystem calls to hasAssignableMVar (#13219) This PR moves `hasAssignableMVar`, `hasAssignableLevelMVar`, and `isLevelMVarAssignable` from `MetavarContext.lean` to a new `Lean.Meta.HasAssignableMVar` module, changing them from generic `[Monad m] [MonadMCtx m]` functions to `MetaM` functions. This enables adding `checkSystem` calls in the recursive traversal, which ensures cancellation and heartbeat checks happen during what can be a very expensive computation. All callers of these functions were already in `MetaM`, so this change is safe. The motivating case is the `4595_slowdown.lean` test, where `hasAssignableMVar` (with `PersistentHashMap.find?` lookups on `mctx.lDepth`) was the dominant CPU cost during elaboration of category theory definitions. Without `checkSystem` calls, cancellation requests could be delayed by over 2 seconds. The test file `4595_slowdown.lean` gets a slightly increased `maxHeartbeats` limit because `checkSystem` now detects heartbeat exhaustion mid-traversal rather than after the function returns. Co-authored-by: Claude Opus 4.6 --- src/Lean/Meta.lean | 1 + src/Lean/Meta/AppBuilder.lean | 1 + src/Lean/Meta/HasAssignableMVar.lean | 60 ++++++++++++++++++++++ src/Lean/Meta/LevelDefEq.lean | 1 + src/Lean/Meta/Sym/Pattern.lean | 1 + src/Lean/Meta/Tactic/Grind/EMatch.lean | 1 + src/Lean/Meta/Tactic/Simp/Rewrite.lean | 1 + src/Lean/MetavarContext.lean | 30 ----------- tests/elab/4595_slowdown.lean | 2 + tests/elab/4595_slowdown.lean.out.expected | 22 ++++---- 10 files changed, 79 insertions(+), 41 deletions(-) create mode 100644 src/Lean/Meta/HasAssignableMVar.lean diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 420e36efb3..816489e3a1 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura module prelude public import Lean.Meta.Basic +public import Lean.Meta.HasAssignableMVar public import Lean.Meta.LevelDefEq public import Lean.Meta.WHNF public import Lean.Meta.InferType diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index d5998c6a73..c6230e3956 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -8,6 +8,7 @@ prelude public import Lean.Meta.SynthInstance public import Lean.Meta.DecLevel import Lean.Meta.CtorRecognizer +public import Lean.Meta.HasAssignableMVar import Lean.Structure import Init.Omega public section diff --git a/src/Lean/Meta/HasAssignableMVar.lean b/src/Lean/Meta/HasAssignableMVar.lean new file mode 100644 index 0000000000..3932f439cd --- /dev/null +++ b/src/Lean/Meta/HasAssignableMVar.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module + +prelude +public import Lean.Meta.Basic + +public section + +open Lean + +namespace Lean.Meta + +def isLevelMVarAssignable (mvarId : LMVarId) : MetaM Bool := do + let mctx ← getMCtx + match mctx.lDepth.find? mvarId with + | some d => return d >= mctx.levelAssignDepth + | _ => panic! s!"unknown universe metavariable {mvarId.name}" + +def hasAssignableLevelMVar : Level → MetaM Bool + | .succ lvl => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl + | .max lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) + | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) + | .mvar mvarId => isLevelMVarAssignable mvarId + | .zero => return false + | .param _ => return false + +/-- Return `true` iff expression contains a metavariable that can be assigned. -/ +partial def hasAssignableMVar (e : Expr) : MetaM Bool := + if !e.hasMVar then + return false + else + go e |>.run' {} +where + go (e : Expr) : StateRefT ExprSet MetaM Bool := + match e with + | .const _ lvls => lvls.anyM (liftM <| hasAssignableLevelMVar ·) + | .sort lvl => liftM <| hasAssignableLevelMVar lvl + | .app f a => do checkSystem "hasAssignableMVar"; visit f <||> visit a + | .letE _ t v b _ => do checkSystem "hasAssignableMVar"; visit t <||> visit v <||> visit b + | .forallE _ d b _ => do checkSystem "hasAssignableMVar"; visit d <||> visit b + | .lam _ d b _ => do checkSystem "hasAssignableMVar"; visit d <||> visit b + | .fvar _ => return false + | .bvar _ => return false + | .lit _ => return false + | .mdata _ e => visit e + | .proj _ _ e => visit e + | .mvar mvarId => mvarId.isAssignable + visit (e : Expr) : StateRefT ExprSet MetaM Bool := do + if !e.hasMVar then return false + if (← get).contains e then return false + modify fun s => s.insert e + go e + +end Lean.Meta + +end diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean index 4ca0e1d9fc..eaed3886b7 100644 --- a/src/Lean/Meta/LevelDefEq.lean +++ b/src/Lean/Meta/LevelDefEq.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Util.CollectMVars public import Lean.Meta.DecLevel +public import Lean.Meta.HasAssignableMVar public section diff --git a/src/Lean/Meta/Sym/Pattern.lean b/src/Lean/Meta/Sym/Pattern.lean index 2d67a4c1f8..6c6f10faa8 100644 --- a/src/Lean/Meta/Sym/Pattern.lean +++ b/src/Lean/Meta/Sym/Pattern.lean @@ -18,6 +18,7 @@ import Lean.Meta.Sym.AlphaShareBuilder import Lean.Meta.Sym.Offset import Lean.Meta.Sym.Eta import Lean.Meta.Sym.Util +import Lean.Meta.HasAssignableMVar import Init.Data.List.MapIdx import Init.Data.Nat.Linear import Std.Do.Triple.Basic diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index 259bec431a..804c4abd9d 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean @@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.SynthInstance import Lean.Meta.Tactic.Grind.Simp import Init.Grind.Util import Init.Omega +public import Lean.Meta.HasAssignableMVar public section namespace Lean.Meta.Grind namespace EMatch diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 1ca46b5bb3..49d1c5d503 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Simp.Arith public import Lean.Meta.Tactic.Simp.Attr public import Lean.Meta.BinderNameHint import Lean.Meta.WHNF +public import Lean.Meta.HasAssignableMVar public section namespace Lean.Meta.Simp /-- diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 0c95664f56..a5fb2c3b87 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -444,12 +444,6 @@ def _root_.Lean.MVarId.isAssignedOrDelayedAssigned [Monad m] [MonadMCtx m] (mvar let mctx ← getMCtx return mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId -def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do - let mctx ← getMCtx - match mctx.lDepth.find? mvarId with - | some d => return d >= mctx.levelAssignDepth - | _ => panic! s!"unknown universe metavariable {mvarId.name}" - def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl := match mctx.decls.find? mvarId with | some decl => decl @@ -484,30 +478,6 @@ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool | .proj _ _ e => pure e.hasMVar <&&> hasAssignedMVar e | .mvar mvarId => mvarId.isAssigned <||> mvarId.isDelayedAssigned -/-- Return true iff the given level contains a metavariable that can be assigned. -/ -def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool - | .succ lvl => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl - | .max lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) - | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) - | .mvar mvarId => isLevelMVarAssignable mvarId - | .zero => return false - | .param _ => return false - -/-- Return `true` iff expression contains a metavariable that can be assigned. -/ -def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool - | .const _ lvls => lvls.anyM hasAssignableLevelMVar - | .sort lvl => hasAssignableLevelMVar lvl - | .app f a => (pure f.hasMVar <&&> hasAssignableMVar f) <||> (pure a.hasMVar <&&> hasAssignableMVar a) - | .letE _ t v b _ => (pure t.hasMVar <&&> hasAssignableMVar t) <||> (pure v.hasMVar <&&> hasAssignableMVar v) <||> (pure b.hasMVar <&&> hasAssignableMVar b) - | .forallE _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b) - | .lam _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b) - | .fvar _ => return false - | .bvar _ => return false - | .lit _ => return false - | .mdata _ e => pure e.hasMVar <&&> hasAssignableMVar e - | .proj _ _ e => pure e.hasMVar <&&> hasAssignableMVar e - | .mvar mvarId => mvarId.isAssignable - /-- Add `mvarId := u` to the universe metavariable assignment. This method does not check whether `mvarId` is already assigned, nor does it check whether diff --git a/tests/elab/4595_slowdown.lean b/tests/elab/4595_slowdown.lean index 7024152182..a86d9e3af4 100644 --- a/tests/elab/4595_slowdown.lean +++ b/tests/elab/4595_slowdown.lean @@ -1,6 +1,8 @@ -- The final declaration blew up by a factor of about 40x heartbeats on an earlier draft of -- https://github.com/leanprover/lean4/pull/4595, so this is here as a regression test. +set_option maxHeartbeats 400000 + universe v v₁ v₂ v₃ u u₁ u₂ u₃ section Mathlib.Combinatorics.Quiver.Basic diff --git a/tests/elab/4595_slowdown.lean.out.expected b/tests/elab/4595_slowdown.lean.out.expected index b52c7fef95..0d6f6a45ec 100644 --- a/tests/elab/4595_slowdown.lean.out.expected +++ b/tests/elab/4595_slowdown.lean.out.expected @@ -1,12 +1,12 @@ -4595_slowdown.lean:104:14-104:25: warning: declaration uses `sorry` -4595_slowdown.lean:136:9-136:17: warning: declaration uses `sorry` -4595_slowdown.lean:154:8-154:16: warning: declaration uses `sorry` -4595_slowdown.lean:181:8-181:14: warning: declaration uses `sorry` +4595_slowdown.lean:106:14-106:25: warning: declaration uses `sorry` +4595_slowdown.lean:138:9-138:17: warning: declaration uses `sorry` +4595_slowdown.lean:156:8-156:16: warning: declaration uses `sorry` 4595_slowdown.lean:183:8-183:14: warning: declaration uses `sorry` -4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry` -4595_slowdown.lean:194:8-194:19: warning: declaration uses `sorry` -4595_slowdown.lean:197:8-197:15: warning: declaration uses `sorry` -4595_slowdown.lean:207:4-207:13: warning: declaration uses `sorry` -4595_slowdown.lean:229:8-229:14: warning: declaration uses `sorry` -4595_slowdown.lean:231:8-231:16: warning: declaration uses `sorry` -4595_slowdown.lean:233:4-233:11: warning: declaration uses `sorry` +4595_slowdown.lean:185:8-185:14: warning: declaration uses `sorry` +4595_slowdown.lean:188:0-188:8: warning: declaration uses `sorry` +4595_slowdown.lean:196:8-196:19: warning: declaration uses `sorry` +4595_slowdown.lean:199:8-199:15: warning: declaration uses `sorry` +4595_slowdown.lean:209:4-209:13: warning: declaration uses `sorry` +4595_slowdown.lean:231:8-231:14: warning: declaration uses `sorry` +4595_slowdown.lean:233:8-233:16: warning: declaration uses `sorry` +4595_slowdown.lean:235:4-235:11: warning: declaration uses `sorry`