From d0505c2e6223ceeb1d42862cda27512fbf189ce4 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Tue, 18 Mar 2025 00:13:13 +0000 Subject: [PATCH 1/3] fix: use `withFreshZetaDeltaFVarIds` to avoid leaking `zetaDeltaFVarIds` between different `simp` calls --- src/Lean/Elab/MutualDef.lean | 1 - src/Lean/Meta/Basic.lean | 21 ++++++++++++++------- src/Lean/Meta/Closure.lean | 1 - 3 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 5f346bd00eca..c6b96141d9b2 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -958,7 +958,6 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai let letRecsToLift := letRecsToLift.toArray let mainFVarIds := mainFVars.map Expr.fvarId! let recFVarIds := (letRecsToLift.map fun toLift => toLift.fvarId) ++ mainFVarIds - resetZetaDeltaFVarIds withTrackingZetaDelta do -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`. let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index b54ca0e2ebb6..002f15cf214e 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -681,8 +681,15 @@ def getConfig : MetaM Config := def getConfigWithKey : MetaM ConfigWithKey := return (← getConfig).toConfigWithKey -def resetZetaDeltaFVarIds : MetaM Unit := - modify fun s => { s with zetaDeltaFVarIds := {} } +@[inline] def withFreshZetaDeltaFVarIds (x : MetaM α) : MetaM α := do + let fvarIdsSaved ← modifyGet fun s => (s.zetaDeltaFVarIds, { s with zetaDeltaFVarIds := {} }) + try + x + finally + if (← read).trackZetaDelta then + modify fun s => { s with zetaDeltaFVarIds := fvarIdsSaved.union s.zetaDeltaFVarIds } + else + modify fun s => { s with zetaDeltaFVarIds := fvarIdsSaved } def getZetaDeltaFVarIds : MetaM FVarIdSet := return (← get).zetaDeltaFVarIds @@ -1117,7 +1124,7 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true` -/ @[inline] def withTrackingZetaDelta : n α → n α := - mapMetaM fun x => + mapMetaM fun x => withFreshZetaDeltaFVarIds <| withFreshCache <| withReader (fun ctx => { ctx with trackZetaDelta := true }) x /-- @@ -1125,21 +1132,21 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true` The cache is reset while executing `x` if `s` is not empty. -/ def withZetaDeltaSet (s : FVarIdSet) : n α → n α := - mapMetaM fun x => + mapMetaM fun x => withFreshZetaDeltaFVarIds <| if s.isEmpty then x else - withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s }) x + withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := ctx.zetaDeltaSet.union s }) x /-- Similar to `withZetaDeltaSet`, but also enables `withTrackingZetaDelta` if `s` is not empty. -/ def withTrackingZetaDeltaSet (s : FVarIdSet) : n α → n α := - mapMetaM fun x => + mapMetaM fun x => withFreshZetaDeltaFVarIds <| if s.isEmpty then x else - withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s, trackZetaDelta := true }) x + withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := ctx.zetaDeltaSet.union s, trackZetaDelta := true }) x @[inline] def withoutProofIrrelevance (x : n α) : n α := withConfig (fun cfg => { cfg with proofIrrelevance := false }) x diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 6aa6578055d4..ec27f7db4666 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -342,7 +342,6 @@ structure MkValueTypeClosureResult where exprArgs : Array Expr def mkValueTypeClosureAux (type : Expr) (value : Expr) : ClosureM (Expr × Expr) := do - resetZetaDeltaFVarIds withTrackingZetaDelta do let type ← collectExpr type let value ← collectExpr value From df05564c6322b7f5d4bb120d03a5ce9d7c9d028c Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Tue, 18 Mar 2025 00:29:58 +0000 Subject: [PATCH 2/3] add test --- tests/lean/zetaDeltaFVarIdsLeakage.lean | 13 +++++++++++++ .../lean/zetaDeltaFVarIdsLeakage.lean.expected.out | 2 ++ 2 files changed, 15 insertions(+) create mode 100644 tests/lean/zetaDeltaFVarIdsLeakage.lean create mode 100644 tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out diff --git a/tests/lean/zetaDeltaFVarIdsLeakage.lean b/tests/lean/zetaDeltaFVarIdsLeakage.lean new file mode 100644 index 000000000000..dbf01a304dfe --- /dev/null +++ b/tests/lean/zetaDeltaFVarIdsLeakage.lean @@ -0,0 +1,13 @@ +example : True := by + let a := 1 + let b := 2 + have : b = 2 := by simp [a,b] + have : a = 1 := by simp? [a] + have : 1 = 1 := by simp? + trivial + +example : False := by + let a := 1 + let b := 1 + have : a = 1 → False := sorry + simp (disch := simp [b]) [this, a] diff --git a/tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out b/tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out new file mode 100644 index 000000000000..2a3b2e617694 --- /dev/null +++ b/tests/lean/zetaDeltaFVarIdsLeakage.lean.expected.out @@ -0,0 +1,2 @@ +Try this: simp only [a] +Try this: simp only From bd4c98aac7d6f6b9a0db37bc6f36d24469139e62 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Tue, 18 Mar 2025 01:07:13 +0000 Subject: [PATCH 3/3] fix test --- tests/lean/zetaDeltaFVarIdsLeakage.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/lean/zetaDeltaFVarIdsLeakage.lean b/tests/lean/zetaDeltaFVarIdsLeakage.lean index dbf01a304dfe..7c8987f0de4f 100644 --- a/tests/lean/zetaDeltaFVarIdsLeakage.lean +++ b/tests/lean/zetaDeltaFVarIdsLeakage.lean @@ -6,8 +6,10 @@ example : True := by have : 1 = 1 := by simp? trivial +axiom test_sorry {α : Sort _} : α + example : False := by let a := 1 let b := 1 - have : a = 1 → False := sorry + have : a = 1 → False := test_sorry simp (disch := simp [b]) [this, a]