From 0199efad3eba36269727dd651a3424670750407e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 31 Jul 2026 19:10:14 +0000 Subject: [PATCH 1/3] feat: restrict and record option accesses during type class resolution This PR makes type class resolution cache entries depend on the options they observed: a query records every result-relevant option lookup (`Lean.getRecordedOption`), and an entry is served only while its recorded lookups give the same answers, so options no longer have to invalidate the cache wholesale (nor silently fail to). Options resolved once per query, such as the definitional-equality compatibility flags and the resource limits, are part of the cache key instead. Acquiring the options plainly is what a running query forbids: `getOptions` panics while `Core.Context.recordingDeps` is set, so nothing can go unrecorded. Type class resolution is a closed system, so the few readers whose result cannot influence a cached entry acquire them through the new `MonadOptions.getOptionsUnrestricted`, each carrying its one-line argument (trace and profiler collection, message rendering, diagnostics counters, and limits whose excess throws and is never cached). The marker is scoped to the computation rather than carried by the options value or the environment, both of which outlive the query in contexts captured for later rendering. The reachable set was measured rather than estimated: over the full `tests/elab` pile a recording query acquires the options 4.3M times from 17 source sites, all of them either audited unrestricted readers or the cache machinery itself. Co-Authored-By: Claude Fable 5 Co-Authored-By: Claude Opus 5 --- src/Lean/CoreM.lean | 80 +++++++++- src/Lean/Data/Options.lean | 12 +- src/Lean/Environment.lean | 24 +++ src/Lean/Message.lean | 9 +- src/Lean/Meta/Basic.lean | 103 ++++++++++++- src/Lean/Meta/Diagnostics.lean | 5 +- src/Lean/Meta/ExprDefEq.lean | 21 +-- src/Lean/Meta/SynthInstance.lean | 202 +++++++++++++++++++++----- src/Lean/Meta/WHNF.lean | 6 +- src/Lean/Util/SafeExponentiation.lean | 4 +- src/Lean/Util/Trace.lean | 18 ++- stage0/src/stdlib_flags.h | 4 +- tests/elab/tc_cache_options.lean | 33 +++++ tests/lake/tests/kinds/produced.out | 1 + 14 files changed, 450 insertions(+), 72 deletions(-) create mode 100644 tests/elab/tc_cache_options.lean diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 61d372630f94..6744b4db1d8f 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -200,6 +200,16 @@ structure State where traceState : TraceState := {} /-- Cache for instantiating universe polymorphic declarations. -/ cache : Cache := {} + /-- + Dependencies observed by the computation currently recording, if any + (`Core.Context.recordingDeps`); becomes the dependency log of the entry it caches, see + `Lean.Meta.SynthInstanceCache` for the only current client. Deliberately *not* backtrackable: + `SavedState.restore` does not restore it, so dependencies observed on a path that is later + rolled back are kept. Recording more than the surviving path observed is benign + over-approximation; losing an observation would not be. For the same reason it does not live + in `Meta.Cache`, which `Meta.modifyEnv` clears wholesale. + -/ + recordedDeps : RecordedDeps := {} /-- Message log. -/ messages : MessageLog := {} /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/ @@ -243,6 +253,13 @@ structure Context where suppressElabErrors : Bool := false /-- Cache of `Lean.inheritedTraceOptions`. -/ inheritedTraceOptions : Std.HashSet Name := {} + /-- + True while this computation is recording its dependencies into `Core.State.recordedDeps`: + by-name option reads are then restricted to the recording accessors, see + `Lean.getRecordedOption`. Scoped to the computation rather than carried by the environment, + which outlives it in captured display contexts. + -/ + recordingDeps : Bool := false deriving Nonempty /-- CoreM is a monad for manipulating the Lean environment. @@ -272,11 +289,25 @@ instance : MonadEnv CoreM where modifyEnv f := modify fun s => { s with env := f s.env, cache := {} } instance : MonadOptions CoreM where - getOptions := return (← read).options + getOptions := do + let ctx ← read + let options := ctx.options + if ctx.recordingDeps then + -- The options are returned from the panic so that a violation reports once instead of + -- cascading through code that would otherwise see every option unset. + have : Inhabited Options := ⟨options⟩ + return panic! "options acquired inside a computation recording its dependencies; \ + result-relevant reads must go through `Lean.getRecordedOption`, all others through \ + `getOptionsUnrestricted`" + return options + getOptionsUnrestricted := return (← read).options instance : MonadWithOptions CoreM where withOptions f x := do - let options := f (← read).options + -- unrestricted acquisition: the reads below see either an unchanged value or a write by `f` + -- done during recording, and both are part of the resolution cache key + -- (`Lean.Meta.SynthInstanceCacheKey.limits`) + let options := f (← getOptionsUnrestricted) let diag := diagnostics.get options if Kernel.isDiagnosticsEnabled (← getEnv) != diag then modifyEnv fun env => Kernel.enableDiag env diag @@ -328,8 +359,12 @@ instance : Elab.MonadInfoTree CoreM where modifyInfoState f := modify fun s => { s with infoState := f s.infoState } @[inline] def modifyCache (f : Cache → Cache) : CoreM Unit := - modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, messages, infoState, snaps⟩ => - ⟨env, next, ngen, auxDeclNGen, trace, f cache, messages, infoState, snaps⟩ + modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, deps, messages, infoState, snaps⟩ => + ⟨env, next, ngen, auxDeclNGen, trace, f cache, deps, messages, infoState, snaps⟩ + +@[inline] def modifyRecordedDeps (f : RecordedDeps → RecordedDeps) : CoreM Unit := + modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, deps, messages, infoState, snaps⟩ => + ⟨env, next, ngen, auxDeclNGen, trace, cache, f deps, messages, infoState, snaps⟩ @[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit := modifyCache fun ⟨c₁, c₂⟩ => ⟨f c₁, c₂⟩ @@ -393,6 +428,9 @@ itself after calling `act` as well as by reuse-handling code such as the one sup @[specialize] def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState)) (act : CoreM α) : CoreM (α × SavedState) := do if let some (val, state) := reusableResult? then + -- Restoring a full state rolls back `State.recordedDeps`, which must not happen while a + -- computation is recording; incremental reuse operates between commands. + assert! !(← read).recordingDeps set state.toState IO.addHeartbeats state.passedHeartbeats return (val, state) @@ -477,7 +515,8 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := { } def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do - let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions) + -- unrestricted acquisition: only reached when the heartbeat limit throws, which is never cached + let includeModuleName := debug.moduleNameAtTimeout.get (← getOptionsUnrestricted) let atModuleName := if includeModuleName then s!" at `{moduleName}`" else "" throw <| Exception.error (← getRef) <| .tagged `runtime.maxHeartbeats m!"\ (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\ @@ -566,6 +605,10 @@ def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelT let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild setDeclNGen parentDeclNGen let st ← get + -- The forked action's final state is discarded below, so anything it records into + -- `State.recordedDeps` is lost: a recording computation must not fork. To be revisited when it + -- becomes necessary. + assert! !(← read).recordingDeps let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen } let ctx ← read let ctx := { ctx with cancelTk? } @@ -767,6 +810,33 @@ where doCompile := do def compileDecl (decl : Declaration) (logErrors := true) : CoreM Unit := do compileDecls (Compiler.getDeclNamesForCodeGen decl) logErrors +/-- Records the lookup `access` in the recording computation's accumulator, if any; see `getRecordedOption`. -/ +private def recordOptionAccess (access : RecordedOptionAccess) : CoreM Unit := do + if (← read).recordingDeps then + -- Read-before-write: repeated lookups of the same option dominate (e.g. per `isDefEq` step), + -- and the membership test avoids the state update for them. + let d := (← get).recordedDeps + unless d.options.any (·.name == access.name) do + Core.modifyRecordedDeps fun ⟨options⟩ => ⟨options.push access⟩ + +/-- +Reads an option inside a recording computation, recording the lookup as an option dependency +of the entry being computed (`Core.State.recordedDeps`); see `Lean.Meta.SynthInstanceCache` for +the only current client. The read bypasses the options restriction, which exists to divert +result-relevant by-name reads to this function; outside a recording computation it behaves like +`Lean.Option.get`. +-/ +def getRecordedOption [KVMap.Value α] (opt : Lean.Option α) : CoreM α := do + let raw := (← getOptionsUnrestricted).find? opt.name + recordOptionAccess { name := opt.name, value := raw } + return (raw.bind KVMap.Value.ofDataValue?).getD opt.defValue + +/-- By-name variant of `getRecordedOption`, for options that cannot be referenced directly. -/ +def getRecordedBoolOption (name : Name) (defVal := false) : CoreM Bool := do + let raw := (← getOptionsUnrestricted).find? name + recordOptionAccess { name, value := raw } + return (raw.bind KVMap.Value.ofDataValue?).getD defVal + def getDiag (opts : Options) : Bool := diagnostics.get opts diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 875b0607fba2..bf8b10c0a5ab 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -50,7 +50,7 @@ instance : EmptyCollection Options where def find := find? @[inline] def get? {α : Type} [KVMap.Value α] (o : Options) (k : Name) : Option α := - o.map.find? k |>.bind KVMap.Value.ofDataValue? + o.find? k |>.bind KVMap.Value.ofDataValue? @[inline] def get {α : Type} [KVMap.Value α] (o : Options) (k : Name) (defVal : α) : α := o.get? k |>.getD defVal @@ -147,11 +147,19 @@ def getOptionDescr (name : Name) : IO String := do class MonadOptions (m : Type → Type) where getOptions : m Options + /-- + Acquires the options without the recording check of `getOptions`, for readers whose result + provably cannot influence a computation that records its dependencies (trace and profiler + collection, message rendering, diagnostics counters, limits whose excess throws and is never + cached). Each use carries a one-line argument; see `Lean.getRecordedOption`. + -/ + getOptionsUnrestricted : m Options := getOptions -export MonadOptions (getOptions) +export MonadOptions (getOptions getOptionsUnrestricted) instance [MonadLift m n] [MonadOptions m] : MonadOptions n where getOptions := liftM (getOptions : m _) + getOptionsUnrestricted := liftM (getOptionsUnrestricted : m _) variable [Monad m] [MonadOptions m] diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 33928512dadc..d93e56023fed 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -540,6 +540,30 @@ private structure RealizationContext where -/ realizeMapRef : IO.Ref (NameMap NonScalar /- PHashMap α (Task Dynamic) -/) +/-- +One option lookup observed by a recording computation: the raw `Options.find?` result, so that +validation is default-independent and covers set↔unset transitions exactly. See +`Lean.getRecordedOption`. +-/ +structure RecordedOptionAccess where + name : Name + value : Option DataValue + deriving BEq + +/-- +What a recording computation observed about its environment and options, accumulated in +`Lean.Core.State.recordedDeps` while it runs; replaying the observations decides whether a +result cached by that computation is still valid. Type class resolution is currently the only +client, see `Lean.Meta.SynthInstance`. +-/ +structure RecordedDeps where + /-- + The option lookups performed, deduplicated by name; a cached result may only be reused when + these lookups give the same answers in the current context. + -/ + options : Array RecordedOptionAccess := #[] + deriving Inhabited + /-- Elaboration-specific extension of `Kernel.Environment` that adds tracking of asynchronously elaborated declarations. diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 5e2281389fe2..11cbf177f171 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -811,15 +811,17 @@ instance (m n) [MonadLift m n] [AddMessageContext m] : AddMessageContext n where addMessageContext := fun msg => liftM (addMessageContext msg : m _) def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do + -- unrestricted acquisition: a message context is a display context, whose later reads cannot + -- influence a cached resolution result let env ← getEnv - let opts ← getOptions + let opts ← getOptionsUnrestricted return MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do let env ← getEnv let mctx ← getMCtx let lctx ← getLCtx - let opts ← getOptions + let opts ← getOptionsUnrestricted return MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData class ToMessageData (α : Type) where @@ -862,7 +864,8 @@ def toMessageList (msgs : Array MessageData) : MessageData := namespace Kernel.Exception private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData := - MessageData.withContext { env := .ofKernelEnv env, mctx := {}, lctx := lctx, opts := opts } msg + MessageData.withContext + { env := .ofKernelEnv env, mctx := {}, lctx := lctx, opts } msg def toMessageData (e : Kernel.Exception) (opts : Options) : MessageData := match e with diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index e207f8f137bd..1abf8dbfb2a4 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -350,6 +350,43 @@ structure InfoCacheKey where instance : Hashable InfoCacheKey where hash := private fun { configKey, expr, nargs? } => mixHash (hash configKey) <| mixHash (hash expr) (hash nargs?) +/-- +The option lookups a type class resolution cache entry was computed under, deduplicated by name; +a lookup may only use an entry whose recorded accesses give the same answers in the current +context. See `SynthInstanceCache`. +-/ +abbrev SynthOptionAccessLog := Array RecordedOptionAccess + +/-- +Resource limits a type class resolution query runs under; part of the cache key, see +`SynthInstanceCacheKey.limits`. +-/ +structure SynthLimits where + maxHeartbeats : Nat + synthInstanceHeartbeats : Nat + maxRecDepth : Nat + exponentiationThreshold : Nat + deriving Hashable, BEq, Inhabited + +/-- +The definitional-equality and unfolding compatibility flags, resolved and recorded once per type +class resolution query (`synthInstanceCore?`) so that their per-step reads inside the search +avoid the recording accessors; see `getSynthDefEqFlag`. Being resolved up front, they are part +of the cache key (`SynthInstanceCacheKey.defEqFlags`) rather than recorded dependencies: every +query partitions on all of them, whether its search reaches the corresponding reads or not. +They are global compatibility settings, so the sharing lost to this over-approximation is +negligible. +-/ +structure SynthDefEqFlags where + respectTransparency : Bool + respectTransparencyTypes : Bool + implicitBump : Bool + reducibleClassField : Bool + lazyProjDelta : Bool + lazyWhnfCore : Bool + smartUnfolding : Bool + deriving Inhabited, BEq, Hashable + -- Remark: we don't need to store `Config.toKey` because typeclass resolution uses a fixed configuration. structure SynthInstanceCacheKey where localInsts : LocalInstances @@ -359,6 +396,27 @@ structure SynthInstanceCacheKey where See issue #2522. -/ synthPendingDepth : Nat + /-- + Effective maximum result size (`synthInstance.maxSize` unless overridden by the caller). + The cache persists across commands, so results (in particular failures) obtained under a + different size limit must not be reused. + -/ + maxResultSize : Nat + /-- + The definitional-equality flags the query runs under, resolved up front; see + `SynthDefEqFlags`. Options read lazily during the search are recorded per entry instead + (`SynthOptionAccessLog`). + -/ + defEqFlags : SynthDefEqFlags + /-- + The resource limits in effect for the query (`maxHeartbeats`, `synthInstance.maxHeartbeats`, + `maxRecDepth`, `exponentiation.threshold`). Exceeding a limit throws, and results are only + cached on the success path, so a limit cannot influence a stored result; keying by them + nevertheless makes that a structural property rather than an argument about exception paths, + and lets their (frequent, mostly out-of-query) reads be plain unrestricted reads. Limits are + effectively constant per module, so this does not partition the cache in practice. + -/ + limits : SynthLimits deriving Hashable, BEq /-- Resulting type for `abstractMVars` -/ @@ -371,7 +429,20 @@ structure AbstractMVarsResult where def AbstractMVarsResult.numMVars (r : AbstractMVarsResult) : Nat := r.mvars.size -abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult) +/-- +Type class resolution cache. Each key holds one entry per observed combination of dependencies: +the search records every result-relevant option lookup (`getRecordedOption`) and every observed +environment dependency (accessed `.recorded` extensions and reducibility statuses; see +`Lean.EnvExtension.TCResolutionAccess`) into the entry's `SynthDepLog`, and a lookup may only +use an entry whose recorded dependencies give the same answers in the current context. +Dependencies the search never observed do not partition the cache. The search observes no other +options or extensions, as it runs with `Core.Context.recordingDeps` set, which diverts option +acquisitions to the recording +`Core.Context.recordingDeps` set, which divert by-name option reads to the recording +accessors and panic on `.deny` extension accesses. +-/ +abbrev SynthInstanceCache := + PersistentHashMap SynthInstanceCacheKey (List (RecordedDeps × Option AbstractMVarsResult)) -- Key for `InferType` and `WHNF` caches structure ExprConfigCacheKey where @@ -411,6 +482,12 @@ abbrev DefEqCache := PersistentHashMap DefEqCacheKey Bool /-- Cache datastructures for type inference, type class resolution, whnf, and definitional equality. + +The `synthInstance` field is the *transient* tier of the type class resolution cache: it has +the lifetime of the current `Meta.State` and holds all entries, including context-sensitive ones +(keys containing metavariables, or results with abstracted metavariables) whose validity is tied +to the current elaboration context. Context-free entries are additionally stored in an +environment extension so that they persist across commands (see `synthInstanceCacheExt`). -/ structure Cache where inferType : InferTypeCache := {} @@ -526,6 +603,8 @@ structure Context where Remark: `synthPending` fails if `synthPendingDepth > maxSynthPendingDepth`. -/ synthPendingDepth : Nat := 0 + /-- Set per type class resolution query; see `SynthDefEqFlags`. -/ + synthDefEqFlags? : Option SynthDefEqFlags := none /-- A predicate to control whether a constant can be unfolded or not at `whnf`. If set, overrides `Config.canUnfoldPredicateConfig`. @@ -1212,6 +1291,19 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : @[inline] def withIncSynthPending : n α → n α := mapMetaM <| withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) +/-- +Reads a definitional-equality compatibility flag: from the per-query resolved flags inside a +type class resolution query, and via `fallback` from the ambient options otherwise. Inside a +query the flags are always armed and already recorded (`SynthDefEqFlags`), so the read costs a +context projection; per-step read sites in `isDefEq`/`whnf` use this instead of the recording +accessors. +-/ +@[inline] def getSynthDefEqFlag (proj : SynthDefEqFlags → Bool) (fallback : Options → Bool) : + MetaM Bool := do + match (← read).synthDefEqFlags? with + | some flags => return proj flags + | none => return fallback (← getOptions) + @[inline] def withInTypeClassResolution : n α → n α := mapMetaM <| withReader (fun ctx => { ctx with inTypeClassResolution := true }) @@ -2270,7 +2362,8 @@ def instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnot return (res, e) def getPPContext : MetaM PPContext := do - return { env := (← getEnv), mctx := (← getMCtx), lctx := (← getLCtx), opts := (← getOptions), + -- unrestricted acquisition: a message context is a display context, see `addMessageContextFull` + return { env := (← getEnv), mctx := (← getMCtx), lctx := (← getLCtx), opts := (← getOptionsUnrestricted), currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls) } /-- Pretty-print the given expression. -/ @@ -2591,7 +2684,8 @@ def instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr := do return e def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do - profileitM Exception s!"instantiate metavars" (← getOptions) do + -- unrestricted acquisition: profiler collection cannot influence a cached resolution result + profileitM Exception s!"instantiate metavars" (← getOptionsUnrestricted) do withTraceNode `Meta.instantiateMVars (fun _ => pure e) do instantiateMVars e @@ -2745,7 +2839,8 @@ def realizeConst (forConst : Name) (constName : Name) (realize : MetaM Unit) : let exAct ← Core.wrapAsyncAsSnapshot (cancelTk? := none) fun | none => return | some ex => do - logError <| ex.toMessageData (← getOptions) + -- unrestricted acquisition: rendering an exception, which is never cached + logError <| ex.toMessageData (← getOptionsUnrestricted) Core.logSnapshotTask { stx? := none task := (← BaseIO.mapTask (t := exTask) exAct) diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean index d1b9c832edb7..0d3e3ae57110 100644 --- a/src/Lean/Meta/Diagnostics.lean +++ b/src/Lean/Meta/Diagnostics.lean @@ -39,7 +39,8 @@ def DiagSummary.isEmpty (s : DiagSummary) : Bool := s.data.isEmpty def mkDiagSummary (cls : Name) (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do - let threshold := diagnostics.threshold.get (← getOptions) + -- unrestricted acquisition: diagnostics counters cannot influence a cached resolution result + let threshold := diagnostics.threshold.get (← getOptionsUnrestricted) let entries := collectAboveThreshold counters threshold p Name.lt if entries.isEmpty then return {} @@ -103,7 +104,7 @@ def reportDiag : MetaM Unit := do let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible let m := appendSection m `type_class "used instances" inst let m := appendSection m `type_class - s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth `" + s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptionsUnrestricted)}), use `set_option maxSynthPendingDepth `" synthPending (resultSummary := false) let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu let m := appendSection m `reduction "Axioms (possibly imported non-exposed defs) that were tried to be unfolded" unfoldAxiom diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index c5cc39145b4c..e2e7eb706693 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -376,8 +376,8 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta for i in finfo.paramInfo.size...args₁.size do unless (← Meta.isExprDefEqAux args₁[i]! args₂[i]!) do return false - let respectTransparency := backward.isDefEq.respectTransparency.get (← getOptions) - let implicitBump := backward.isDefEq.implicitBump.get (← getOptions) + let respectTransparency ← getSynthDefEqFlag (·.respectTransparency) (backward.isDefEq.respectTransparency.get ·) + let implicitBump ← getSynthDefEqFlag (·.implicitBump) (backward.isDefEq.implicitBump.get ·) for i in postponedImplicit do /- Second pass: unify implicit arguments. When `respectTransparency` is `false` (old behavior), we bump to `.default` so that @@ -485,9 +485,9 @@ and is used to enable the transparency bump when checking metavariable assignmen If `backward.isDefEq.respectTransparency` is `false`, then we automatically disable `backward.isDefEq.respectTransparency.types` too. -/ -abbrev respectTransparencyAtTypes : CoreM Bool := do - let opts ← getOptions - return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts +abbrev respectTransparencyAtTypes : MetaM Bool := do + return (← getSynthDefEqFlag (·.respectTransparencyTypes) (backward.isDefEq.respectTransparency.types.get ·)) + && (← getSynthDefEqFlag (·.respectTransparency) (backward.isDefEq.respectTransparency.get ·)) private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do @@ -1445,7 +1445,7 @@ private def isNonTrivialRegular (info : DefinitionVal) : MetaM Bool := do only applies there. At higher transparency levels, the normal unfolding behavior is sufficient, and running the heuristic adds overhead without benefit. See https://github.com/leanprover/lean4/pull/12650 -/ - return projInfo.fromClass && backward.whnf.reducibleClassField.get (← getOptions) && (← getTransparency) == .reducible + return projInfo.fromClass && (← getSynthDefEqFlag (·.reducibleClassField) (backward.whnf.reducibleClassField.get ·)) && (← getTransparency) == .reducible return false | .opaque => return false where @@ -1758,7 +1758,7 @@ private def etaEq (t s : Expr) : Bool := performance foot-gun. Users can use the backward compatibility flag to restore the old behavior. -/ private def withProofIrrelTransparency (k : MetaM α) : MetaM α := do - if backward.isDefEq.respectTransparency.get (← getOptions) then + if (← getSynthDefEqFlag (·.respectTransparency) (backward.isDefEq.respectTransparency.get ·)) then k else withInferTypeConfig k @@ -2112,7 +2112,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool if (← read).inTypeClassResolution then -- See comment at `inTypeClassResolution` pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s) - else if !backward.isDefEq.lazyProjDelta.get (← getOptions) then + else if !(← getSynthDefEqFlag (·.lazyProjDelta) (backward.isDefEq.lazyProjDelta.get ·)) then pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s) else if i == j && m == n then isDefEqStructArgs (isDefEqProjDelta t s i) @@ -2275,7 +2275,7 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un modifyDefEqTransientCache fun c => c.insert key result private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do - if backward.isDefEq.lazyWhnfCore.get (← getOptions) then + if (← getSynthDefEqFlag (·.lazyWhnfCore) (backward.isDefEq.lazyWhnfCore.get ·)) then withConfig (fun ctx => { ctx with proj := .yesWithDeltaI }) <| whnfCore e else whnfCore e @@ -2284,7 +2284,8 @@ set_option compiler.ignoreBorrowAnnotation true in @[export lean_is_expr_def_eq] partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do withTraceNodeBefore `Meta.isDefEq (fun _ => do - if trace.Meta.isDefEq.printTransparency.get (← getOptions) then + -- unrestricted read: trace collection cannot influence a cached resolution result + if trace.Meta.isDefEq.printTransparency.get (← getOptionsUnrestricted) then return m!"[{toString (← getTransparency)}] {t} =?= {s}" else return m!"{t} =?= {s}") do diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 450d8edb60c6..c3bae2912411 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -598,7 +598,7 @@ def generate : SynthM Unit := do let mctx := gNode.mctx let mvar := gNode.mvar /- See comment at `typeHasMVars` -/ - if backward.synthInstance.canonInstances.get (← getOptions) then + if (← getRecordedOption backward.synthInstance.canonInstances) then unless gNode.typeHasMVars do if let some entry := (← get).tableEntries[key]? then if entry.answers.any fun answer => answer.result.numMVars == 0 then @@ -680,7 +680,9 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult newSubgoal (← getMCtx) key mvar Waiter.root synth tryCatchRuntimeEx - (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {}) + -- unrestricted acquisition: the limit is part of the resolution cache key + -- (`SynthInstanceCacheKey.limits`) + (action.run { maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptionsUnrestricted) } |>.run' {}) fun ex => if ex.isRuntime then throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}{useDiagnosticMsg}" @@ -921,6 +923,73 @@ private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVa check result return some result +/-- Returns whether every recorded lookup in `log` gives the same answer in `opts`. -/ +private def validOptionAccesses (opts : Options) (log : SynthOptionAccessLog) : Bool := + log.all fun a => opts.find? a.name == a.value + +/-- +Merges the dependencies observed by a nested query (or served from a used cache entry) into the +enclosing query's accumulator: the enclosing query observed the nested result, so it depends on +whatever the nested one did. +-/ +private def _root_.Lean.RecordedDeps.mergeInto (child parent : RecordedDeps) : RecordedDeps := + let options := child.options.foldl (init := parent.options) fun l a => + if l.any (·.name == a.name) then l else l.push a + { parent with options } + +/-- +Identity of two dependency logs for entry replacement in `insertCachedResult`: the same option +lookups with the same answers. +-/ +private def sameDepIdentity (a b : RecordedDeps) : Bool := + a.options == b.options + +/-- +Inserts a result into the type class resolution cache (`Meta.Cache.synthInstance`), which has +the lifetime of the current `Meta.State`; note that `Meta.SavedState.restore` deliberately does +not restore `Meta.Cache`, so entries survive backtracking (e.g. tactics trying alternatives) +within a command. +-/ +private def insertCachedResult (key : SynthInstanceCacheKey) (log : RecordedDeps) + (result? : Option AbstractMVarsResult) : MetaM Unit := do + -- One entry per observed dependency combination; replace an entry with the same identity. + let upsert (c : SynthInstanceCache) : SynthInstanceCache := + c.insert key <| (log, result?) :: (c.find? key |>.getD [] |>.filter fun e => !sameDepIdentity e.1 log) + modifyCache fun c => { c with synthInstance := upsert c.synthInstance } + +/-- +Validates a cache entry's recorded dependencies against the current context: every recorded +option lookup must give the same answer. Returns `none` if the entry may not be used. +-/ +private def validateDeps? (opts : Options) (_env : Environment) + (log : RecordedDeps) : BaseIO (Option (RecordedDeps × Bool)) := do + unless validOptionAccesses opts log.options do return none + return some (log, false) + +/-- +Returns the type class resolution cache entry for `key` from the transient +(`Meta.Cache.synthInstance`), together with its recorded dependencies. Only entries whose +recorded dependencies give the same answers in the current context are considered +(`validateDeps?`); a re-stamped entry is re-inserted. See `SynthInstanceCache`. +-/ +private def findCachedResult? (key : SynthInstanceCacheKey) : + MetaM (Option (RecordedDeps × Option AbstractMVarsResult)) := do + -- unrestricted acquisition: only compared against recorded lookups (`validOptionAccesses`) + let opts ← getOptionsUnrestricted + let env ← getEnv + let findIn (c : SynthInstanceCache) : + BaseIO (Option (RecordedDeps × Option AbstractMVarsResult × Bool)) := do + let some entries := c.find? key | return none + for (log, val?) in entries do + if let some (log, restamped) ← validateDeps? opts env log then + return some (log, val?, restamped) + return none + if let some (log, val?, restamped) ← findIn (← get).cache.synthInstance then + if restamped then + insertCachedResult key log val? + return some (log, val?) + return none + /-- Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthInstance.main` into an `Expr`. This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`. @@ -940,42 +1009,89 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr applyAbstractResult? type abstResult? /-- Helper function for caching synthesized type class instances. -/ -private def cacheResult (cacheKey : SynthInstanceCacheKey) (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do - -- **TODO**: simplify this function. - match abstResult? with - | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none } - | some abstResult => - if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then - match result? with - | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none } - | some result => - -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced, - -- we don't need to perform extra checks again when reusing result. - modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], mvars := #[] }) } - else - modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) } +private def cacheResult (cacheKey : SynthInstanceCacheKey) (log : RecordedDeps) (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do + -- The stored value: for a closed result we store the concrete `result` expr with an empty + -- `AbstractMVarsResult` so that `applyCachedAbstractResult?` can skip re-`check`ing it. + let value? := + match abstResult? with + | none => none + | some abstResult => + if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then + result?.map fun result => { expr := result, paramNames := #[], mvars := #[] } + else + some abstResult + insertCachedResult cacheKey log value? + +/-- +The `Meta.Config` used for all type class resolution. The ambient configuration is replaced +wholesale rather than adjusted: resolution results are cached across contexts and commands with no +configuration component in the cache key, so any ambient configuration that influenced the search +(e.g. `canUnfoldPredicateConfig` set by `simp`) would leak between contexts through the cache. +Search-relevant state that must flow in from the caller is context, not configuration, and is part +of the cache key (e.g. `synthPendingDepth`, the relevant options). +-/ +private def synthInstanceConfig : Config := + { isDefEqStuckEx := true, transparency := .instances, + foApprox := true, ctxApprox := true, constApprox := false, univApprox := false } def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do - let opts ← getOptions - let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts) + -- For a nested query this read happens under the enclosing query's restriction and is recorded + -- as its dependency: the value determines the nested query's cache key. + let maxResultSize ← match maxResultSize? with + | some n => pure n + | none => getRecordedOption synthInstance.maxSize + -- The query's dependencies: result-relevant option lookups on the search path go through the + -- recording accessors (`getRecordedOption`) and flow into the accumulator + -- `Core.State.recordedDeps`, which becomes the cache entry's dependency log, see + -- `SynthInstanceCache`. The enclosing query's accumulator (if any) is saved here and the + -- nested query's effective dependencies are merged into it on exit (`finally` below): the + -- enclosing query observed the result. + let parentDeps := (← getThe Core.State).recordedDeps + let parentRecording := (← readThe Core.Context).recordingDeps + modifyThe Core.State fun s => { s with recordedDeps := {} } + try + -- Mark the query as recording; the marker is scoped to the search, so only the accumulator + -- has to be restored below. + withTheReader Core.Context (fun ctx => { ctx with recordingDeps := true }) do + -- Resolve the per-step definitional-equality flags once; they are part of the cache key + -- rather than recorded dependencies, so the raw reads are not logged. See `SynthDefEqFlags`. + -- Unrestricted acquisition: everything read below is part of the key. + let opts ← getOptionsUnrestricted + let getB (n : Name) (d : Bool) : Bool := + ((opts.find? n).bind KVMap.Value.ofDataValue?).getD d + let flags : SynthDefEqFlags := { + respectTransparency := getB `backward.isDefEq.respectTransparency true + respectTransparencyTypes := getB `backward.isDefEq.respectTransparency.types true + implicitBump := getB `backward.isDefEq.implicitBump true + reducibleClassField := getB `backward.whnf.reducibleClassField true + lazyProjDelta := getB `backward.isDefEq.lazyProjDelta true + lazyWhnfCore := getB `backward.isDefEq.lazyWhnfCore true + smartUnfolding := getB `smartUnfolding true + } + -- Resource limits are part of the cache key (`SynthInstanceCacheKey.limits`): exceeding one + -- throws and results are only stored on the success path, so a limit cannot influence a + -- stored result, and keying by them makes that structural. Read by name because their + -- accessors live in modules this one does not import. + let getN (n : Name) (d : Nat) : Nat := + ((opts.find? n).bind KVMap.Value.ofDataValue?).getD d + let limits : SynthLimits := { + maxHeartbeats := getN `maxHeartbeats 200000 + synthInstanceHeartbeats := getN `synthInstance.maxHeartbeats 20000 + maxRecDepth := getN `maxRecDepth 512 + exponentiationThreshold := getN `exponentiation.threshold 256 + } + withReader (fun ctx => { ctx with synthDefEqFlags? := some flags }) do withTraceNode `Meta.synthInstance (fun _ => return m!"{← instantiateMVars type}") do - withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances, - foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do + withConfig (fun _ => synthInstanceConfig) do withInTypeClassResolution do let localInsts ← getLocalInstances let type ← instantiateMVars type let { type, cacheKeyType, kind } ← preprocess type - let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth } - match (← get).cache.synthInstance.find? cacheKey with - | some abstResult? => - trace[Meta.synthInstance.cache] "cached: {type}" - let result? ← applyCachedAbstractResult? type abstResult? - trace[Meta.synthInstance] "result {result?} (cached)" - return result? - | none => - trace[Meta.synthInstance.cache] "new: {type}" - let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do + let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth, + maxResultSize, defEqFlags := flags, limits } + let runSearch : MetaM (Option AbstractMVarsResult) := + withNewMCtxDepth (allowLevelAssignments := true) do match kind with | .noMVars => /- @@ -1000,12 +1116,30 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met SynthInstance.main (← preprocessOutParam type) maxResultSize | .mvarsNoOutputParams => SynthInstance.main type maxResultSize | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize + match ← findCachedResult? cacheKey with + | some (entryLog, abstResult?) => + trace[Meta.synthInstance.cache] "cached: {type}" + -- The used entry's dependencies become dependencies of this query. + modifyThe Core.State fun s => { s with recordedDeps := entryLog.mergeInto s.recordedDeps } + let result? ← applyCachedAbstractResult? type abstResult? + trace[Meta.synthInstance] "result {result?} (cached)" + return result? + | none => + trace[Meta.synthInstance.cache] "new: {type}" + let abstResult? ← runSearch let result? ← applyAbstractResult? type abstResult? trace[Meta.synthInstance] "result {result?}" - cacheResult cacheKey kind abstResult? result? + cacheResult cacheKey ((← getThe Core.State).recordedDeps) kind abstResult? result? return result? - -def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do + finally + -- Restore the enclosing accumulator, merging this query's effective dependencies into it. + let childDeps := (← getThe Core.State).recordedDeps + modifyThe Core.State fun s => { s with recordedDeps := + if parentRecording then childDeps.mergeInto parentDeps else parentDeps } + +def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do + -- unrestricted acquisition: profiler collection cannot influence a cached resolution result + profileitM Exception "typeclass inference" (← getOptionsUnrestricted) (decl := type.getAppFn.constName?.getD .anonymous) do synthInstanceCore? type maxResultSize? /-- @@ -1041,7 +1175,7 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| | none => return false | some _ => - let max := maxSynthPendingDepth.get (← getOptions) + let max ← getRecordedOption maxSynthPendingDepth if (← read).synthPendingDepth > max then trace[Meta.synthPending] "too many nested synthPending invocations" recordSynthPendingFailure mvarDecl.type diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 059e41e77244..bd4c88d82703 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -822,7 +822,7 @@ private def unfoldDefault (fInfo : ConstantInfo) (us : List Level) (e : Expr) : if fInfo.hasValue then recordUnfold fInfo.name deltaBetaDefinition fInfo us e.getAppRevArgs (fun _ => pure none) fun e => do - if !backward.whnf.reducibleClassField.get (← getOptions) then + if !(← getSynthDefEqFlag (·.reducibleClassField) (backward.whnf.reducibleClassField.get ·)) then return some e else if !(← getTransparency) matches .reducible then return some e @@ -850,7 +850,7 @@ mutual else let unfoldDefault (_ : Unit) : MetaM (Option Expr) := unfoldDefault fInfo fLvls e - if smartUnfolding.get (← getOptions) then + if (← getSynthDefEqFlag (·.smartUnfolding) (smartUnfolding.get ·)) then match ((← getEnv).find? (skipRealize := true) (mkSmartUnfoldingNameFor fInfo.name)) with | some fAuxInfo@(.defnInfo _) => -- We use `preserveMData := true` to make sure the smart unfolding annotation are not erased in an over-application. @@ -915,7 +915,7 @@ mutual let some cinfo ← getConstInfoNoEx? declName ignoreTransparency | pure none -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a -- significant chance of not existing and `Environment.contains` misses are more costly - if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then + if (← getSynthDefEqFlag (·.smartUnfolding) (smartUnfolding.get ·)) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then return none else unless cinfo.hasValue do diff --git a/src/Lean/Util/SafeExponentiation.lean b/src/Lean/Util/SafeExponentiation.lean index 476983a5900b..fa5bdc21b747 100644 --- a/src/Lean/Util/SafeExponentiation.lean +++ b/src/Lean/Util/SafeExponentiation.lean @@ -27,7 +27,9 @@ reports a warning and returns `false`. This method ensures there is at most one warning message of this kind in the message log. -/ def checkExponent (n : Nat) (warning := true) : CoreM Bool := do - let threshold := exponentiation.threshold.get (← getOptions) + -- unrestricted acquisition: the threshold is part of the resolution cache key + -- (`Lean.Meta.SynthInstanceCacheKey.limits`) + let threshold := exponentiation.threshold.get (← getOptionsUnrestricted) if n > threshold then if (← pure warning <&&> logMessageKind `unsafe.exponentiation) then logWarning s!"exponent {n} exceeds the threshold {threshold}, exponentiation operation was not evaluated, use `set_option {exponentiation.threshold.name} ` to set a new threshold" diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 4d441f69db37..837bad02ca76 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -106,7 +106,7 @@ def resetTraceState : m Unit := opts.hasTrace && go (`trace ++ cls) where go (opt : Name) : Bool := - if let some enabled := opts.get? opt then + if let some enabled := (opts.find? opt).bind KVMap.Value.ofDataValue? then enabled else if let .str parent _ := opt then inherited.contains opt && go parent @@ -116,7 +116,8 @@ where /-- Determine if tracing is available for a given class, checking ancestor classes if appropriate. -/ @[inline] def isTracingEnabledFor (cls : Name) : m Bool := do - return checkTraceOption (← MonadTrace.getInheritedTraceOptions) (← getOptions) cls + -- unrestricted acquisition: trace collection cannot influence a cached resolution result + return checkTraceOption (← MonadTrace.getInheritedTraceOptions) (← getOptionsUnrestricted) cls @[export lean_is_trace_class_enabled] private def isTracingEnabledForExport (opts : Options) (cls : Name) : BaseIO Bool := do @@ -211,7 +212,7 @@ True if the `trace.profiler` data should be retained for export - either to a fi that would otherwise consume the trace state as messages must leave it intact. -/ @[inline] def trace.profiler.isExporting (opts : Options) : Bool := - (trace.profiler.output.get? opts).isSome || trace.profiler.serve.get opts + (opts.find? trace.profiler.output.name).isSome || trace.profiler.serve.get opts register_builtin_option trace.profiler.output.pp : Bool := { defValue := false @@ -332,7 +333,9 @@ The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToTraceResult ε α] (cls : Name) (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do - let opts ← getOptions + -- unrestricted acquisition here and in `postCallback`: trace and profiler collection cannot + -- influence a cached resolution result + let opts ← getOptionsUnrestricted if !opts.hasTrace then return (← k) let clsEnabled ← isTracingEnabledFor cls @@ -415,7 +418,9 @@ TODO: find better name for this function. def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m] [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToTraceResult ε α] (cls : Name) (msg : Unit → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do - let opts ← getOptions + -- unrestricted acquisition here and in `postCallback`: trace and profiler collection cannot + -- influence a cached resolution result + let opts ← getOptionsUnrestricted if !opts.hasTrace then return (← k) let clsEnabled ← isTracingEnabledFor cls @@ -445,7 +450,8 @@ where MonadExcept.ofExcept res def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Unit := do - if trace.profiler.isExporting (← getOptions) then + -- unrestricted acquisition: profiler collection cannot influence a cached resolution result + if trace.profiler.isExporting (← getOptionsUnrestricted) then -- do not add trace messages if the profile is being exported (`trace.profiler.output` or -- `trace.profiler.serve`) as it would be redundant, pretty printing the trace messages is -- expensive, and `getResetTraces` would consume the data we want to export diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 3baec9ac0fdd..bfd7e2768544 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -16,14 +16,14 @@ options get_option_overrides() { // uncomment for ABI-breaking changes affecting meta code; // see also next option! - //opts = opts.update({"interpreter", "prefer_native"}, true); + opts = opts.update({"interpreter", "prefer_native"}, true); // comment out when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this should usually be done, but setting // both to `true` may be necessary for handling non-builtin parsers with // builtin elaborators // TODO: make consistent across stages - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); + //opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); // changes to builtin parsers may also require uncommenting the following option if macros/syntax // with custom precheck hooks were affected diff --git a/tests/elab/tc_cache_options.lean b/tests/elab/tc_cache_options.lean new file mode 100644 index 000000000000..63295d051feb --- /dev/null +++ b/tests/elab/tc_cache_options.lean @@ -0,0 +1,33 @@ +import Lean.Elab.Command + +/-! +Tests that the type class resolution cache tracks options by *recorded accesses*: a query +records every result-relevant option lookup it performs (`Lean.getRecordedOption`), and an +entry is served only while those lookups give the same answers. Options the search never read +do not partition the cache; options it did read do. +-/ + +open Lean Meta Elab Command + +class Boo (α : Type) where + +instance : Boo Nat := ⟨⟩ + +/-- +trace: [Meta.synthInstance.cache] new: Boo Nat +[Meta.synthInstance.cache] cached: Boo Nat +[Meta.synthInstance.cache] cached: Boo Nat +[Meta.synthInstance.cache] new: Boo Nat +-/ +#guard_msgs in +run_cmd liftTermElabM do + let ty := mkApp (mkConst ``Boo) (mkConst ``Nat) + let query : TermElabM Unit := + withOptions (·.setBool `trace.Meta.synthInstance.cache true) do + discard <| synthInstance? ty + query + query + -- A result-irrelevant option the search never reads does not partition the cache. + withOptions (·.setBool `pp.universes true) do query + -- `backward.synthInstance.canonInstances` is read by the search, so it does. + withOptions (·.setBool `backward.synthInstance.canonInstances false) do query diff --git a/tests/lake/tests/kinds/produced.out b/tests/lake/tests/kinds/produced.out index e69de29bb2d1..280bc4e62bfa 100644 --- a/tests/lake/tests/kinds/produced.out +++ b/tests/lake/tests/kinds/produced.out @@ -0,0 +1 @@ +dynlib From 0dfdf36acd632be157bf10ac9eae9eb4328d13a1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 8 Aug 2026 09:09:29 +0000 Subject: [PATCH 2/3] feat: record and validate environment dependencies of type class resolution cache entries This PR makes type class resolution cache entries depend on the environment state they observed, completing the dependency tracking begun with option accesses. Extensions the search consults are classified at registration: generation-tracked extensions (instances, unification hints) are read through recording accessors that log the observed generation, and covered extensions hold declaration-keyed content whose observable changes are enforced by the write machinery rather than trusted. A read of an unclassified extension during a query panics, and `tests/elab/tc_cache_covered_claims.lean` locks that audit. Declaration-keyed writes are guarded for value stability, and a write some recording query could have observed is appended to a change log validated by constant birth ordering: the environment assigns each constant a per-lineage birth index as it becomes observable, so a change whose target was born after an entry was recorded cannot have affected it. Reducibility attribute changes are the most common such write. `debug.synthInstance.checkCacheHits` additionally re-runs served cache hits from scratch and compares, as a differential soak check. The recording marker gains a second home on the environment (`Environment.isRecordingDeps`) alongside the scoped `Core.Context.recordingDeps` introduced with option recording. Extension reads are pure functions of an environment, with no monad to consult, so this is the only marker they can see; the two are armed together and a captured display context (messages, pretty printing) clears the environment one at the boundary. Co-Authored-By: Claude Fable 5 --- src/Lean/Attributes.lean | 14 +- src/Lean/AuxRecursor.lean | 12 +- src/Lean/Class.lean | 3 + src/Lean/CoreM.lean | 17 +- src/Lean/DeclarationRange.lean | 4 +- src/Lean/DocString/Add.lean | 7 +- src/Lean/DocString/Extension.lean | 4 +- src/Lean/Elab/BuiltinEvalCommand.lean | 1 - src/Lean/Elab/Command.lean | 8 +- .../PreDefinition/PartialFixpoint/Eqns.lean | 4 +- .../Elab/PreDefinition/Structural/Eqns.lean | 3 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 3 +- src/Lean/EnvExtension.lean | 41 ++- src/Lean/Environment.lean | 334 +++++++++++++++--- src/Lean/Message.lean | 7 +- src/Lean/Meta/Basic.lean | 28 +- .../Meta/Constructions/SparseCasesOn.lean | 17 +- src/Lean/Meta/Eqns.lean | 18 +- src/Lean/Meta/Instances.lean | 46 ++- src/Lean/Meta/Match/MatchEqsExt.lean | 18 +- src/Lean/Meta/Match/MatchPatternAttr.lean | 5 +- src/Lean/Meta/Match/MatcherInfo.lean | 2 + src/Lean/Meta/MethodSpecs.lean | 12 +- src/Lean/Meta/SynthInstance.lean | 129 +++++-- src/Lean/Meta/UnificationHint.lean | 7 +- src/Lean/ProjFns.lean | 8 +- src/Lean/ReducibilityAttrs.lean | 40 ++- src/Lean/ResolveName.lean | 4 +- src/Lean/ScopedEnvExtension.lean | 47 ++- src/Lean/Structure.lean | 28 +- src/Lean/Util/PPExt.lean | 16 +- tests/elab/tc_cache_check_hits.lean | 34 ++ tests/elab/tc_cache_covered_claims.lean | 76 ++++ tests/elab/tc_cache_reducibility_birth.lean | 45 +++ 34 files changed, 898 insertions(+), 144 deletions(-) create mode 100644 tests/elab/tc_cache_check_hits.lean create mode 100644 tests/elab/tc_cache_covered_claims.lean create mode 100644 tests/elab/tc_cache_reducibility_birth.lean diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 0dc4a0096c05..ae1b5ad83685 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -180,9 +180,11 @@ structure TagAttribute where def registerTagAttribute (name : Name) (descr : String) (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) (applicationTime := AttributeApplicationTime.afterTypeChecking) - (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagAttribute := do + (asyncMode : EnvExtension.AsyncMode := .mainOnly) + (declCovered : Bool := false) : IO TagAttribute := do let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension { name := ref + declCovered := declCovered mkInitial := pure {} addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameSet) n => s.insert n @@ -210,7 +212,11 @@ def registerTagAttribute (name : Name) (descr : String) unless ext.toEnvExtension.asyncMayModify env decl do throwAttrNotInAsyncCtx name decl env.asyncPrefix? validate decl - modifyEnv fun env => ext.addEntry (asyncDecl := decl) env decl + modifyEnv fun env => + -- a post-hoc application some recording query could have observed must be recorded for + -- covered attributes; see `Environment.declChangeLog` + let env := if declCovered then env.logDeclChange decl else env + ext.addEntry (asyncDecl := decl) env decl } registerBuiltinAttribute attrImpl return { attr := attrImpl, ext := ext } @@ -262,10 +268,12 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where def registerParametricAttributeExt (ref : Name) (preserveOrder : Bool := false) (filterExport : Environment → Name → α → Bool := fun env n _ => - env.contains (skipRealize := false) n) : + env.contains (skipRealize := false) n) + (declCovered : Bool := false) : IO (PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) := registerPersistentEnvExtension { name := ref + declCovered := declCovered mkInitial := pure ([], {}) addImportedFn := fun _ => pure ([], {}) addEntryFn := fun (decls, m) (p : Name × α) => (p.1 :: decls, m.insert p.1 p.2) diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean index b906750f4904..e9f4f1b911ec 100644 --- a/src/Lean/AuxRecursor.lean +++ b/src/Lean/AuxRecursor.lean @@ -23,7 +23,9 @@ def mkRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName recOnSuf def mkBRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName brecOnSuffix def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix -builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension (asyncMode := .async .mainEnv) +builtin_initialize auxRecExt : TagDeclarationExtension ← + -- covered: aux-recursor status is an immutable per-declaration fact + mkTagDeclarationExtension (asyncMode := .async .mainEnv) (declCovered := true) def markAuxRecursor (env : Environment) (declName : Name) : Environment := auxRecExt.tag env declName @@ -50,7 +52,9 @@ def isRecOnRecursor (env : Environment) (declName : Name) : Bool := def isBRecOnRecursor (env : Environment) (declName : Name) : Bool := isAuxRecursorWithSuffix env declName brecOnSuffix -private builtin_initialize sparseCasesOnExt : TagDeclarationExtension ← mkTagDeclarationExtension (asyncMode := .async .mainEnv) +private builtin_initialize sparseCasesOnExt : TagDeclarationExtension ← + -- covered: sparse-`casesOn` status is an immutable per-declaration fact + mkTagDeclarationExtension (asyncMode := .async .mainEnv) (declCovered := true) def markSparseCasesOn (env : Environment) (declName : Name) : Environment := sparseCasesOnExt.tag env declName @@ -79,7 +83,9 @@ def NoConfusionInfo.arity : NoConfusionInfo → Nat | .regular arity _ _ => arity | .perCtor arity _ => arity -builtin_initialize noConfusionExt : MapDeclarationExtension NoConfusionInfo ← mkMapDeclarationExtension (asyncMode := .mainOnly) +builtin_initialize noConfusionExt : MapDeclarationExtension NoConfusionInfo ← + -- covered: `noConfusion` facts are immutable per declaration and monotone + mkMapDeclarationExtension (asyncMode := .mainOnly) (declCovered := true) def markNoConfusion (env : Environment) (n : Name) (info : NoConfusionInfo) : Environment := noConfusionExt.insert env n info diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index 79b457a08230..40bedf71dc7f 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -69,8 +69,11 @@ Type class environment extension -- TODO: add support for scoped instances builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ← registerSimplePersistentEnvExtension { + -- covered: class facts are immutable per declaration and monotone + declCovered := true addEntryFn := ClassState.addEntry addImportedFn := fun es => (mkStateFromImportedEntries ClassState.addEntry {} es).switch + -- class facts are immutable per declaration and monotone } /-- Return `true` if `n` is the name of type class in the given environment. -/ diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 6744b4db1d8f..c52a83be9221 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -817,7 +817,22 @@ private def recordOptionAccess (access : RecordedOptionAccess) : CoreM Unit := d -- and the membership test avoids the state update for them. let d := (← get).recordedDeps unless d.options.any (·.name == access.name) do - Core.modifyRecordedDeps fun ⟨options⟩ => ⟨options.push access⟩ + Core.modifyRecordedDeps fun ⟨options, extGens, g, p, w⟩ => + ⟨options.push access, extGens, g, p, w⟩ + +/-- +Records the current generation of the generation-tracked extension with registration index +`extIdx` in the recording computation's accumulator, if any; the read-side counterpart of the +`EnvExtension.trackGen` bump. Call sites record the generation through this accessor and then +read the state itself with `(recorded := true)`. +-/ +def recordExtGenAccess (extIdx : Nat) : CoreM Unit := do + if (← read).recordingDeps then + let d := (← get).recordedDeps + unless d.extGens.any (·.1 == extIdx) do + let gen ← EnvExtension.getRecordedGen (← getEnv) extIdx + Core.modifyRecordedDeps fun ⟨options, extGens, g, p, w⟩ => + ⟨options, extGens.push (extIdx, gen), g, p, w⟩ /-- Reads an option inside a recording computation, recording the lookup as an option dependency diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean index 406579133874..70ba790e01c1 100644 --- a/src/Lean/DeclarationRange.lean +++ b/src/Lean/DeclarationRange.lean @@ -29,7 +29,9 @@ def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges : if declName.isAnonymous then -- This can happen on elaboration of partial syntax and would panic in `modifyState` otherwise return - modifyEnv fun env => declRangeExt.insert env declName declRanges + -- position metadata, not resolution-relevant: later writes legitimately refine earlier ones + -- (e.g. structure elaboration re-reports its generated declarations) + modifyEnv fun env => declRangeExt.insert env declName declRanges (allowOverwrite := true) def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) := -- In the case of private definitions imported via `import all`, looking in `.olean.server` is not diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean index 82eb3405a1d5..4dcfd0969bb0 100644 --- a/src/Lean/DocString/Add.lean +++ b/src/Lean/DocString/Add.lean @@ -318,7 +318,9 @@ def addMarkdownDocString throwError m!"invalid doc string, declaration `{.ofConstName declName}` is in an imported module" validateDocComment docComment let docString : String ← getDocStringText docComment - modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces + -- documentation metadata, not resolution-relevant: later writes legitimately replace + -- earlier ones + modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces (allowOverwrite := true) /-- Adds an elaborated Verso docstring to the environment, recording its `deferred` checks under this @@ -333,7 +335,8 @@ def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadErr unless (← getEnv).getModuleIdxFor? declName |>.isNone do throwError s!"invalid doc string, declaration '{declName}' is in an imported module" modifyEnv fun env => - let env := versoDocStringExt.insert env declName docs + -- documentation metadata, as above + let env := versoDocStringExt.insert env declName docs (allowOverwrite := true) deferred.foldl (init := env) fun env c => Doc.deferredCheckExt.addEntry env { c with site := .decl declName } diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean index 8958b216039f..9a50c46b9e08 100644 --- a/src/Lean/DocString/Extension.lean +++ b/src/Lean/DocString/Extension.lean @@ -166,7 +166,9 @@ def getBuiltinVersoDocStrings : IO (NameMap VersoDocString) := def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) (docString : String) : m Unit := do unless (← getEnv).getModuleIdxFor? declName |>.isNone do throwError m!"invalid doc string, declaration `{.ofConstName declName}` is in an imported module" - modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces + -- documentation metadata, not resolution-relevant: later writes legitimately replace + -- earlier ones + modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces (allowOverwrite := true) def removeDocStringCore [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m Unit := do unless (← getEnv).getModuleIdxFor? declName |>.isNone do diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean index 2ec9947250df..7c66d5f9959d 100644 --- a/src/Lean/Elab/BuiltinEvalCommand.lean +++ b/src/Lean/Elab/BuiltinEvalCommand.lean @@ -155,7 +155,6 @@ private def mkFormat (e : Expr) : MetaM Expr := do try trace[Elab.eval] "Attempting to derive a `Repr` instance for `{.ofConstName name}`" liftCommandElabM do applyDerivingHandlers ``Repr #[name] - resetSynthInstanceCache return ← mkRepr e catch ex => trace[Elab.eval] "Failed to use derived `Repr` instance. Exception: {ex.toMessageData}" diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 998561d235aa..017610493754 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -1097,11 +1097,13 @@ such as `open` and `namespace` commands, only have an effect for the remainder of the `CommandElabM` computation passed here, and do not affect subsequent commands. -*Warning:* when using this from `MetaM` monads, the caches are *not* reset. -If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache` -to reset the instance cache. +*Warning:* when using this from `MetaM` monads, the `Meta.Cache` caches are *not* reset. While the `modifyEnv` function for `MetaM` clears its caches entirely, `liftCommandElabM` has no way to reset these caches. +The type class resolution cache is unaffected by this: its entries record their dependencies +and self-invalidate when the command changes them (e.g. by adding instances or changing +reducibility attributes). Other `Meta.Cache` components (e.g. the `whnf` and `isDefEq` caches) +can however retain results invalidated by the command's environment changes. -/ def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : CoreM α := do -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`. diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean index e01bfbfb38c6..ed7726515c03 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean @@ -26,7 +26,9 @@ public structure EqnInfo where deriving Inhabited public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← - mkMapDeclarationExtension (exportEntriesFn := fun env s => + -- covered: consulted by the reserved-name predicates for fixpoint induction names, so also on + -- resolution search paths; populated only when the declaration is created (monotone) + mkMapDeclarationExtension (declCovered := true) (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index bbb0c35cb5e6..6458758e1b04 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -148,7 +148,8 @@ where throwError "no progress at goal\n{MessageData.ofGoal mvarId}" public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← - mkMapDeclarationExtension (exportEntriesFn := fun env s => + -- covered: eqn info is registered when the definition is created (monotone, name-keyed) + mkMapDeclarationExtension (declCovered := true) (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 69a38f359706..3aa557c6ea6b 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -24,7 +24,8 @@ public structure EqnInfo where deriving Inhabited public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← - mkMapDeclarationExtension (exportEntriesFn := fun env s => + -- covered: eqn info is registered when the definition is created (monotone, name-keyed) + mkMapDeclarationExtension (declCovered := true) (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray diff --git a/src/Lean/EnvExtension.lean b/src/Lean/EnvExtension.lean index 83589454bbd2..3450133f01e7 100644 --- a/src/Lean/EnvExtension.lean +++ b/src/Lean/EnvExtension.lean @@ -29,6 +29,9 @@ structure SimplePersistentEnvExtensionDescr (α σ : Type) where Option (Environment → σ → List α → OLeanEntries (Array α)) := none asyncMode : EnvExtension.AsyncMode := .mainOnly replay? : Option ((newEntries : List α) → (newState : σ) → σ → List α × σ) := none + /-- See `EnvExtension.trackGen`. -/ + declCovered : Bool := false + /-- Returns a function suitable for `SimplePersistentEnvExtensionDescr.replay?` that replays all new @@ -53,6 +56,7 @@ def registerSimplePersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : | none => .uniform (descr.toArrayFn s.1.reverse) statsFn := fun s => format "number of local entries: " ++ format s.1.length asyncMode := descr.asyncMode + declCovered := descr.declCovered replay? := descr.replay?.map fun replay oldState newState _ (entries, s) => let newEntries := newState.1.take (newState.1.length - oldState.1.length) let (newEntries, s) := replay newEntries newState.2 s @@ -90,9 +94,11 @@ end SimplePersistentEnvExtension @[expose] def TagDeclarationExtension := SimplePersistentEnvExtension Name NameSet def mkTagDeclarationExtension (name : Name := by exact decl_name%) - (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagDeclarationExtension := + (asyncMode : EnvExtension.AsyncMode := .mainOnly) + (declCovered : Bool := false) : IO TagDeclarationExtension := registerSimplePersistentEnvExtension { name := name, + declCovered := declCovered, addImportedFn := fun _ => {}, addEntryFn := fun s n => s.insert n, toArrayFn := fun es => es.toArray.qsort Name.quickLt @@ -113,7 +119,12 @@ def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) : else have : Inhabited Environment := ⟨env⟩ assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension` - ext.addEntry (asyncDecl := declName) env declName + if ext.getState (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl := declName) env + |>.contains declName then + env -- idempotent re-tag: no observable change, nothing to record + else + let env := if ext.toEnvExtension.declCovered then env.logDeclChange declName else env + ext.addEntry (asyncDecl := declName) env declName def isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) (asyncMode := ext.toEnvExtension.asyncMode) : Bool := @@ -131,14 +142,17 @@ deriving Inhabited def mkMapDeclarationExtension (name : Name := by exact decl_name%) (asyncMode : EnvExtension.AsyncMode := .async .mainEnv) + (declCovered : Bool := false) (exportEntriesFn : Environment → NameMap α → OLeanEntries (Array (Name × α)) := -- Do not export info for private defs by default fun env s => let all := s.toArray.filter (fun (n, _) => env.contains (skipRealize := false) n) - .uniform all) : + .uniform all) + : IO (MapDeclarationExtension α) := .mk <$> registerPersistentEnvExtension { name := name, + declCovered := declCovered, mkInitial := pure {} addImportedFn := fun _ => pure {} addEntryFn := fun s (n, v) => s.insert n v @@ -153,15 +167,29 @@ def mkMapDeclarationExtension (name : Name := by exact decl_name%) namespace MapDeclarationExtension -def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment := +def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) + (allowOverwrite := false) : Environment := have : Inhabited Environment := ⟨env⟩ if let some modIdx := env.getModuleIdxFor? declName then -- See comment at `MapDeclarationExtension` panic! s!"cannot insert `{declName}` into `{ext.name}`, it is not defined in the current module but in `{env.allImportedModuleNames[modIdx]!}`" + -- Write-once guard: dependency-recording coverage claims for declaration-keyed + -- extensions rest on entries being immutable once written (`EnvExtension.trackGen`). Sites + -- that legitimately update an entry must say so (`allowOverwrite`), with a justification. + else if !allowOverwrite && + (ext.toPersistentEnvExtension.getState (asyncDecl := declName) env + |>.contains declName) then + panic! s!"cannot insert `{declName}` into `{ext.name}`, it is already present; \ + declaration-keyed extension entries are immutable once written (pass \ + `allowOverwrite := true` with a justification if this update is intended)" else + -- only covered extensions participate in resolution-cache validation; see + -- `Environment.declChangeLog` + let env := if ext.toEnvExtension.declCovered then env.logDeclChange declName else env ext.addEntry (asyncDecl := declName) env (declName, val) def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) - (asyncMode := ext.toEnvExtension.asyncMode) (level := OLeanLevel.exported) : Option α := + (asyncMode := ext.toEnvExtension.asyncMode) (level := OLeanLevel.exported) + : Option α := match env.getModuleIdxFor? declName with | some modIdx => match (ext.getModuleEntries (level := level) env modIdx).binSearch (declName, default) (fun a b => Name.quickLt a.1 b.1) with @@ -169,7 +197,8 @@ def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) | none => none | none => (ext.getState (asyncMode := asyncMode) (asyncDecl := declName) env).find? declName -def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Bool := +def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) + : Bool := match env.getModuleIdxFor? declName with | some modIdx => (ext.getModuleEntries env modIdx).binSearchContains (declName, default) (fun a b => Name.quickLt a.1 b.1) | none => (ext.getState (asyncDecl := declName) env).contains declName diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index d93e56023fed..782886499983 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -562,6 +562,29 @@ structure RecordedDeps where these lookups give the same answers in the current context. -/ options : Array RecordedOptionAccess := #[] + /-- + Per accessed generation-tracked extension (see `EnvExtension.trackGen`), the state generation + that was observed: `(extension index, generation)`. The dependency is stale once the + extension's generation moves. + -/ + extGens : Array (Nat × Nat) := #[] + /-- + Value of `Environment.recordGen` when recording started. While it is unchanged, none of the + recorded environment dependencies can have changed and validation skips their checks. + -/ + recordGen : Nat := 0 + /-- + Length of the declaration change log (`Environment.declChangeLog`) when recording started. + Changes appended since whose target was born after `constBirthW` are skipped during + validation (the computation cannot have observed a declaration that did not exist yet); any other + change conservatively invalidates the entry. + -/ + changeLogPos : Nat := 0 + /-- + Value of `Environment.constBirthGen` when recording started: the birth watermark for + `changeLogPos`. + -/ + constBirthW : Nat := 0 deriving Inhabited /-- @@ -636,6 +659,46 @@ structure Environment where `elabMutualDef` may switch from public to private when e.g. entering the proof of a theorem. -/ isExporting : Bool := false + /-- + True while a computation is recording its dependencies on this environment branch + (`Lean.Core.State.recordedDeps`): its by-name option reads are restricted to + `Lean.getRecordedOption`, generation-tracked extensions must be read through the recording + accessors (`EnvExtension.trackGen`), and every other extension read must be of a covered + extension (`EnvExtension.declCovered`). + -/ + isRecordingDeps : Bool := false + /-- + Log of declaration-keyed state changes some recording computation could have observed: a write + about a declaration is appended when the declaration was born before the latest arming + (`recordArmBirthGen`); writes about younger declarations cannot falsify any recorded entry and + stay silent. Cache entries are validated against the log by birth arithmetic + (`Environment.checkDeclChangeLog`); reducibility status changes are the most common source. + -/ + declChangeLog : Array Name := #[] + /-- + Value of `Environment.constBirthGen` at the most recent arming of a recording computation on this + lineage; see `declChangeLog`. + -/ + recordArmBirthGen : Nat := 0 + /-- + Counter bumped by every modification a recorded dependency could refer to: any + state change of a generation-tracked extension and every post-hoc reducibility change. Cache + entries are stamped with it (`RecordedDeps.recordGen`); while it is unchanged, validation skips + all per-dependency environment checks. It deliberately does not cover option values, which are + context rather than environment state. + -/ + recordGen : Nat := 0 + /-- + Birth indices of the constants added on this environment lineage, assigned when a constant + becomes observable here (synchronous `addDecl`, asynchronous registration); imported constants + and constants with unknown provenance (e.g. realized constants, currently) are absent and + treated as index 0, older than any watermark, which is the conservative direction. Consumers + capture a watermark (`constBirthGen`) and test `constBirthIdx n > watermark` to prove that a + recording taken at the watermark cannot have observed `n`; see `Environment.declChangeLog`. + -/ + constBirths : PHashMap Name Nat := {} + /-- Watermark counter for `constBirths`. -/ + constBirthGen : Nat := 0 deriving Nonempty @[inline] private def VisibilityMap.get (m : VisibilityMap α) (env : Environment) : α := @@ -680,6 +743,52 @@ def setExporting (env : Environment) (isExporting : Bool) : Environment := else { env with isExporting } +/-- Bumps `env.recordGen`; see there. Called where recorded dependencies change outside `EnvExtension.modifyState`. -/ +def bumpRecordGen (env : Environment) : Environment := + { env with recordGen := env.recordGen + 1 } + +/-- Registers `n` as born now on this environment lineage; see `Environment.constBirths`. -/ +def registerConstBirth (env : Environment) (n : Name) : Environment := + { env with constBirths := env.constBirths.insert n (env.constBirthGen + 1) + constBirthGen := env.constBirthGen + 1 } + +/-- +Birth index of `n` on this lineage; 0 (older than any watermark) for imported constants and +constants of unknown provenance. See `Environment.constBirths`. +-/ +def constBirthIdx (env : Environment) (n : Name) : Nat := + env.constBirths.find? n |>.getD 0 + +/-- +Records a state change about `declName` in `Environment.declChangeLog` if some recording +computation could have observed the pre-change state, i.e. if the declaration was born before +the latest arming; see there. Callers invoke this only for writes that actually change +observable state (idempotent re-registrations stay silent). +-/ +def logDeclChange (env : Environment) (declName : Name) : Environment := + if env.constBirthIdx declName ≤ env.recordArmBirthGen then + -- the log check sits behind the `recordGen` short-circuit, so appends must bump it + { env with declChangeLog := env.declChangeLog.push declName }.bumpRecordGen + else + env + +/-- +Validates the declaration-change dependencies of an entry recorded at log position `fromPos` +with birth watermark `birthW`: every change appended since must +target a declaration born after the watermark; see `Environment.declChangeLog`. +-/ +def checkDeclChangeLog (env : Environment) (fromPos birthW : Nat) : Bool := + fromPos ≤ env.declChangeLog.size && + env.declChangeLog.all (fun d => env.constBirthIdx d > birthW) (start := fromPos) + +/-- Updates `env.isRecordingDeps`; arming also stamps `Environment.recordArmBirthGen`. -/ +def setRecordingDeps (env : Environment) (recording : Bool) : Environment := + if recording then + { env with isRecordingDeps := true, recordArmBirthGen := env.constBirthGen } + else if env.isRecordingDeps then + { env with isRecordingDeps := false } + else env + /-- Consistently updates synchronous and (private) asynchronous parts of the environment without blocking. -/ private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment := { env with checked := env.checked.map (sync := true) f, base.private := f env.base.private } @@ -738,6 +847,7 @@ def addDeclCore (env : Environment) (maxHeartbeats : USize) (maxRecDepth : USize -- visibility scopes but the caller can still customize the public one on the main elaboration -- branch by use of `addConstAsync` as is the case for `Lean.addDecl`. for n in decl.getNames do + env := env.registerConstBirth n let some info := env.checked.get.find? n | unreachable! env := { env with asyncConstsMap.private := env.asyncConstsMap.private.add { constInfo := .ofConstantInfo info @@ -1077,6 +1187,7 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) | some v => .mk v.nestedConsts.public | none => .mk (α := AsyncConsts) default } + let env := env.registerConstBirth constName return { constName, kind, exportedKind? mainEnv := { env with @@ -1346,6 +1457,38 @@ structure EnvExtension (σ : Type) where private mk :: present. -/ replay? : Option (ReplayFn σ) + /-- Name for diagnostics; set automatically for persistent extensions. -/ + name : Name + /-- + Whether the extension state is stored together with a generation counter that every + modification bumps. Type class resolution cache entries depend on extension state in one of + two regimes: + + * *Generation-tracked* (`trackGen`): reads by a recording computation go through the recording + accessors, which record the observed generation as a dependency of the cache entry being + computed, so a state change invalidates exactly the entries that consulted this extension; + see `Lean.Meta.SynthInstance`. A *pure* read while recording panics. For + extensions answering *shape* queries (candidate sets such as instances), where a new + declaration changes answers about pre-existing queries. + * *Covered* (`declCovered`): declaration-keyed content whose observable changes are + enforced by the write machinery rather than trusted: entries are write-stability-guarded + (`MapDeclarationExtension.insert`), and a write some recording computation could have observed + is appended to the declaration change log and validated by birth arithmetic + (`Environment.declChangeLog`, `Environment.constBirths`). Reads are then free everywhere. + The registration site states the extension's coverage argument in one line; the residual + assumption, uniform across covered extensions, is that reads are keyed by declarations + reachable from the computation. + + A read of an unclassified extension while recording panics: a recording computation is a + closed system, so every extension it consults is classifiable at + registration. `tests/elab/tc_cache_covered_claims.lean` locks the audit. + + Must use `AsyncMode.local` or `.mainOnly`: generations are branch-local, matching the + visibility of the resolution cache. + -/ + trackGen : Bool + /-- Whether reads of this extension are covered; see `trackGen` for the classification. -/ + declCovered : Bool deriving Inhabited namespace EnvExtension @@ -1359,13 +1502,23 @@ private builtin_initialize envExtensionsRef : IO.Ref (Array (EnvExtension EnvExt user-defined environment extensions. When this happens, we must adjust the size of the `env.extensions`. This method is invoked when processing `import`s. -/ +private unsafe def mkInitialEntryUnsafe (ext : EnvExtension EnvExtensionState) : IO EnvExtensionState := do + let s ← ext.mkInitial + if ext.trackGen then + return unsafeCast ((0, s) : Nat × EnvExtensionState) + return s + +/-- Creates the state array entry for `ext`; see `modifyStateImpl` for the `.recorded` pairing. -/ +@[implemented_by mkInitialEntryUnsafe] +private opaque mkInitialEntry (ext : EnvExtension EnvExtensionState) : IO EnvExtensionState + partial def ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do loop exts.size exts where loop (i : Nat) (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do let envExtensions ← envExtensionsRef.get if h : i < envExtensions.size then - let s ← envExtensions[i].mkInitial + let s ← mkInitialEntry envExtensions[i] let exts := exts.push s loop (i + 1) exts else @@ -1373,34 +1526,48 @@ where private def invalidExtMsg := "invalid environment extension has been accessed" -private unsafe def setStateImpl {σ} (ext : EnvExtension σ) (exts : Array EnvExtensionState) (s : σ) : Array EnvExtensionState := - if h : ext.idx < exts.size then - exts.set ext.idx (unsafeCast s) - else - -- do not return an empty array on panic, avoiding follow-up out-of-bounds accesses - have : Inhabited (Array EnvExtensionState) := ⟨exts⟩ - panic! invalidExtMsg +/- +For `.recorded` extensions the entry stored in the state array is the state paired with its +generation counter (as `Nat × σ`); all other extensions store the state directly. The pairing is +confined to `modifyStateImpl`/`getStateImpl` and `mkInitialEntry`, which are the only functions +creating or reading entries. +-/ -private unsafe def modifyStateImpl {σ : Type} (ext : EnvExtension σ) (exts : Array EnvExtensionState) (f : σ → σ) : Array EnvExtensionState := +private unsafe def modifyStateImpl {σ : Type} (ext : EnvExtension σ) (exts : Array EnvExtensionState) (f : σ → σ) + (keepRecordGen := false) : Array EnvExtensionState := if ext.idx < exts.size then exts.modify ext.idx fun s => - let s : σ := unsafeCast s - let s : σ := f s - unsafeCast s + if ext.trackGen then + let (gen, s) : Nat × σ := unsafeCast s + unsafeCast ((if keepRecordGen then gen else gen + 1, f s) : Nat × σ) + else + let s : σ := unsafeCast s + let s : σ := f s + unsafeCast s else -- do not return an empty array on panic, avoiding follow-up out-of-bounds accesses have : Inhabited (Array EnvExtensionState) := ⟨exts⟩ panic! invalidExtMsg -private unsafe def getStateImpl {σ} [Inhabited σ] (ext : EnvExtension σ) (exts : Array EnvExtensionState) : σ := +private unsafe def getStateImpl {σ} [Inhabited σ] (ext : EnvExtension σ) (exts : Array EnvExtensionState) + (tripwire : Bool := false) : σ := if h : ext.idx < exts.size then - unsafeCast exts[ext.idx] + if tripwire then + -- an unclaimed read while recording: no recorded dependency validates it + panic! s!"unclassified environment extension read while recording dependencies: \ + `{ext.name}` (index {ext.idx}); the extension should either be registered as covered \ + (`declCovered`, with a justification) or generation-tracked and read through the \ + recording accessors (see `EnvExtension.trackGen`)" + else if ext.trackGen then + (unsafeCast exts[ext.idx] : Nat × σ).2 + else + unsafeCast exts[ext.idx] else panic! invalidExtMsg def mkInitialExtStates : IO (Array EnvExtensionState) := do let exts ← envExtensionsRef.get - exts.mapM fun ext => ext.mkInitial + exts.mapM mkInitialEntry /-- Checks whether `modifyState (asyncDecl := declName)` may be called on an async environment @@ -1424,21 +1591,35 @@ def asyncMayModify (ext : EnvExtension σ) (env : Environment) (asyncDecl : Name Applies the given function to the extension state. See `AsyncMode` for details on how modifications from different environment branches are reconciled. +For generation-tracked extensions the modification bumps the state's generation counter, +invalidating recorded entries that depend on it, unless `keepRecordGen` is set; +see `EnvExtension.trackGen`. + Note that in modes `sync` and `async`, `f` will be called twice, on the local and on the `checked` state. -/ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) - (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) : Environment := Id.run do + (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) + (keepRecordGen := false) : Environment := Id.run do -- for panics let _ : Inhabited Environment := ⟨env⟩ -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ` + -- Only generation-tracked modifications advance an invalidation counter; untracked extension + -- state is validated purely through the read-side covered claims (`EnvExtension.trackGen`). + let bumped (env : Environment) : Environment := + if ext.trackGen && !keepRecordGen then + env.bumpRecordGen + else + env match asyncMode with | .mainOnly => if let some asyncCtx := env.asyncCtx? then return panic! s!"environment extension is marked as `mainOnly` but used in {asyncCtx.descr}" - return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f } + let env := bumped env + return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f keepRecordGen } | .local => - return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f } + let env := bumped env + return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f keepRecordGen } | _ => if asyncMode matches .async _ then if asyncDecl.isAnonymous then @@ -1452,8 +1633,9 @@ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ if let some (n :: _) := env.asyncCtx?.map (·.realizingStack) then return panic! s!"environment extension must set `replay?` field to be \ used in realization context '{n}'" - env.modifyCheckedAsync fun env => - { env with extensions := unsafe ext.modifyStateImpl env.extensions f } + -- `trackGen` extensions cannot use these modes (see `registerEnvExtension`) + (bumped env).modifyCheckedAsync fun env => + { env with extensions := unsafe ext.modifyStateImpl env.extensions f keepRecordGen } /-- Sets the extension state to the given value. See `AsyncMode` for details on how modifications from @@ -1464,10 +1646,17 @@ def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) (a -- `unsafe` fails to infer `Nonempty` here private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension σ) - (env : Environment) (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) : σ := Id.run do + (env : Environment) (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) + (recorded := false) : σ := Id.run do + -- Reads of unclassified extensions and pure reads of generation-tracked extensions panic + -- while recording; see `getStateImpl` and `EnvExtension.trackGen`. `recorded` is + -- internal plumbing for the recording accessors: the caller asserts it has recorded this + -- tracked extension's generation for the current query. + let tripwire := env.isRecordingDeps && + (if ext.trackGen then !recorded else !ext.declCovered) -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ` match asyncMode with - | .sync => ext.getStateImpl env.checked.get.extensions + | .sync => ext.getStateImpl env.checked.get.extensions tripwire | .async branch => if asyncDecl.isAnonymous then panic! "called on `async` extension, must set `asyncDecl` \ @@ -1476,22 +1665,22 @@ private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension -- analogous structure to `findAsync?`; see there -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ` if env.base.get env |>.constants.contains asyncDecl then - return ext.getStateImpl env.base.private.extensions + return ext.getStateImpl env.base.private.extensions tripwire -- specialization of the following branch, nested async decls are rare if let some c := env.asyncConsts.find? asyncDecl then match branch with | .asyncEnv => if let some exts := c.exts? then - return ext.getStateImpl exts.get + return ext.getStateImpl exts.get tripwire else - return ext.getStateImpl env.base.private.extensions + return ext.getStateImpl env.base.private.extensions tripwire | .mainEnv => if c.isRealized then if let some exts := c.exts? then - return ext.getStateImpl exts.get + return ext.getStateImpl exts.get tripwire else - return ext.getStateImpl env.base.private.extensions + return ext.getStateImpl env.base.private.extensions tripwire if let some (c, parent?) := env.asyncConsts.findRecAndParent? asyncDecl then -- If `parent?` is `none`, the current branch is the parent @@ -1505,17 +1694,17 @@ private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension -- this specific case, accessing the latter will in particular not block longer than the -- former. | .mainEnv => if c.isRealized then c.exts? else parentExts?) then - return ext.getStateImpl exts.get + return ext.getStateImpl exts.get tripwire -- NOTE: if `exts?` is `none`, we should *not* try the following, more expensive branches that -- will just come to the same conclusion else if let some c := env.allRealizations.get.find? asyncDecl then if let some exts := c.exts? then - return ext.getStateImpl exts.get + return ext.getStateImpl exts.get tripwire -- fallback; we could enforce that `asyncDecl` and its extension state always exist but the -- upside of doing is unclear and it is not true in e.g. the compiler. One alternative would be -- to add a `getState?` that does not panic in such cases. - ext.getStateImpl env.base.private.extensions - | _ => ext.getStateImpl env.base.private.extensions + ext.getStateImpl env.base.private.extensions tripwire + | _ => ext.getStateImpl env.base.private.extensions tripwire /-- Returns the current extension state. See `AsyncMode` for details on how modifications from @@ -1526,7 +1715,31 @@ only for important optimizations. -/ @[implemented_by getStateUnsafe] opaque getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) - (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) : σ + (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) (recorded := false) : σ + +private unsafe def getGenUnsafe (ext : EnvExtension EnvExtensionState) (env : Environment) : Nat := + -- `.recorded` extensions are restricted to `.local`/`.mainOnly`, whose state lives in the + -- current branch's array. + let exts := env.base.private.extensions + if h : ext.idx < exts.size then + (unsafeCast exts[ext.idx] : Nat × EnvExtensionState).1 + else 0 + +@[implemented_by getGenUnsafe] +private opaque getGen (ext : EnvExtension EnvExtensionState) (env : Environment) : Nat + +/-- +Current generation of the `.recorded` extension with registration index `idx` on the current +branch of `env`, or 0 if `idx` does not denote a `.recorded` extension. Used to validate the +`RecordedDeps.extGens` dependencies of a recorded entry. +-/ +def getRecordedGen (env : Environment) (idx : Nat) : BaseIO Nat := do + let exts ← envExtensionsRef.get + if h : idx < exts.size then + let ext := exts[idx] + if ext.trackGen then + return getGen ext env + return 0 end EnvExtension @@ -1539,12 +1752,19 @@ end EnvExtension For that, you need to register a persistent environment extension. -/ def registerEnvExtension {σ : Type} (mkInitial : IO σ) (replay? : Option (ReplayFn σ) := none) - (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO (EnvExtension σ) := do + (asyncMode : EnvExtension.AsyncMode := .mainOnly) + (name : Name := .anonymous) + (trackGen : Bool := false) + (declCovered : Bool := false) : IO (EnvExtension σ) := do unless (← initializing) do throw (IO.userError "failed to register environment, extensions can only be registered during initialization") + if trackGen then + unless asyncMode matches .local | .mainOnly do + throw (IO.userError "generation-tracked environment extensions must use `AsyncMode.local` or \ + `.mainOnly`; generations are branch-local (see `EnvExtension.trackGen`)") let exts ← EnvExtension.envExtensionsRef.get let idx := exts.size - let ext : EnvExtension σ := { idx, mkInitial, asyncMode, replay? } + let ext : EnvExtension σ := { idx, mkInitial, asyncMode, replay?, name, trackGen, declCovered } -- safety: `EnvExtensionState` is opaque, so we can upcast to it EnvExtension.envExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext) pure ext @@ -1693,12 +1913,13 @@ but is limited to the maximum level actually imported: `exported` on the cmdline language server. Higher levels will return the data of the maximum imported level. -/ def getModuleEntries {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) - (env : Environment) (m : ModuleIdx) (level := OLeanLevel.exported) : Array α := + (env : Environment) (m : ModuleIdx) (level := OLeanLevel.exported) : Array α := Id.run do + -- imported entries are immutable within a module, so reads record no resolution dependency let exts := match level with | .exported => env.base.private.extensions | _ => env.serverBaseExts -- safety: as in `getStateUnsafe` - unsafe (ext.toEnvExtension.getStateImpl exts).importedEntries[m]! + return unsafe (ext.toEnvExtension.getStateImpl exts).importedEntries[m]! /-- Retrieves additional IR extension state for the interpreter. -/ def getModuleIREntries {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) @@ -1714,8 +1935,10 @@ def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En /-- Get the current state of the given extension in the given environment. -/ def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) - (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := .anonymous) : σ := - (ext.toEnvExtension.getState (asyncMode := asyncMode) (asyncDecl := asyncDecl) env).state + (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := .anonymous) + (recorded := false) : σ := + (ext.toEnvExtension.getState (asyncMode := asyncMode) (asyncDecl := asyncDecl) + (recorded := recorded) env).state /-- Set the current state of the given extension in the given environment. -/ def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment := @@ -1723,8 +1946,10 @@ def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En /-- Modify the state of the given extension in the given environment by applying the given function. -/ def modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) - (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := Name.anonymous) : Environment := - ext.toEnvExtension.modifyState (asyncMode := asyncMode) (asyncDecl := asyncDecl) env fun ps => { ps with state := f (ps.state) } + (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := Name.anonymous) + (keepRecordGen := false) : Environment := + ext.toEnvExtension.modifyState (asyncMode := asyncMode) (asyncDecl := asyncDecl) + (keepRecordGen := keepRecordGen) env fun ps => { ps with state := f (ps.state) } end PersistentEnvExtension @@ -1740,6 +1965,10 @@ structure PersistentEnvExtensionDescrCore (α β σ : Type) where statsFn : σ → Format := fun _ => Format.nil asyncMode : EnvExtension.AsyncMode := .mainOnly replay? : Option (ReplayFn σ) := none + /-- See `EnvExtension.trackGen`. -/ + trackGen : Bool := false + /-- See `EnvExtension.trackGen`. -/ + declCovered : Bool := false attribute [inherit_doc PersistentEnvExtension.exportEntriesFn] PersistentEnvExtensionDescrCore.exportEntriesFnEx @@ -1766,7 +1995,8 @@ unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ] if pExts.any (fun ext => ext.name == descr.name) then throw (IO.userError s!"invalid environment extension, '{descr.name}' has already been used") let replay? := descr.replay?.map fun replay => fun oldState newState newConsts s => { s with state := replay oldState.state newState.state newConsts s.state } - let ext ← registerEnvExtension (asyncMode := descr.asyncMode) (replay? := replay?) do + let ext ← registerEnvExtension (asyncMode := descr.asyncMode) (replay? := replay?) + (name := descr.name) (trackGen := descr.trackGen) (declCovered := descr.declCovered) do let initial ← descr.mkInitial let s : PersistentEnvExtensionState α σ := { importedEntries := #[], @@ -2780,6 +3010,14 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name) pure (.mk res) let some res := res.get? RealizeConstResult | unreachable! let exPromise ← IO.Promise.new + -- The realized constants and their extension-state snapshots become observable on this + -- lineage with this merge, so this is where their birth indices are assigned; see + -- `Environment.constBirths`. + let env := res.newConsts.private.foldl (init := env) fun env c => + if env.asyncConstsMap.private.find? c.constInfo.name |>.isSome then + env + else + env.registerConstBirth c.constInfo.name let env := { env with asyncConstsMap := { «private» := res.newConsts.private.foldl (init := env.asyncConstsMap.private) fun consts c => @@ -2905,11 +3143,21 @@ This is consulted for all definitions regardless of their reducibility hints. Cu structural recursion to ensure that parent definitions get the correct height even though the `_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/ builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ← - registerEnvExtension (pure {}) (asyncMode := .local) + -- covered: overrides are declaration-keyed, write-stability-guarded, and logged + registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true) /-- Register a height override for a definition so that `getMaxHeight` uses it. -/ def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment := - defHeightOverrideExt.modifyState env fun m => m.insert declName height + let env := env.logDeclChange declName + defHeightOverrideExt.modifyState env fun m => + -- write-stability guard; see `MapDeclarationExtension.insert` + match m.find? declName with + | some prev => + if prev != height then + panic! s!"definition height override for `{declName}` is already set" + else + m + | none => m.insert declName height def getMaxHeight (env : Environment) (e : Expr) : UInt32 := let overrides := defHeightOverrideExt.getState env diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 11cbf177f171..e52da5269017 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -812,13 +812,14 @@ instance (m n) [MonadLift m n] [AddMessageContext m] : AddMessageContext n where def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do -- unrestricted acquisition: a message context is a display context, whose later reads cannot - -- influence a cached resolution result - let env ← getEnv + -- influence a cached resolution result; the environment's recording marker is dropped so that + -- later extension reads by message consumers do not trip it + let env := (← getEnv).setRecordingDeps false let opts ← getOptionsUnrestricted return MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do - let env ← getEnv + let env := (← getEnv).setRecordingDeps false let mctx ← getMCtx let lctx ← getLCtx let opts ← getOptionsUnrestricted diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 1abf8dbfb2a4..ffabdbf4d377 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -397,6 +397,26 @@ structure SynthInstanceCacheKey where -/ synthPendingDepth : Nat /-- + Namespaces with scoped instances that are currently activated (e.g. via `open`), in canonical + order. Keying the cache by this set keeps entries from outside a scope valid after the scope + ends, e.g. for the `open Classical in` expansion of `by_cases`. + -/ + activeScopedInsts : Array Name + /-- + Instances currently added with the `local` attribute kind (`Instances.localInstanceNames`). + Like `activeScopedInsts`, keying the cache by this set keeps entries from outside a scope + containing `attribute [local instance]` valid after the scope ends, and prevents entries + computed with the local instance from leaking out of the scope. + -/ + localAttrInsts : Array Name + /-- + Instances currently erased via `attribute [-instance]` (`Instances.erased`), in canonical + order. Erasure is delimited by its surrounding scope like local instances, and entries are + keyed by it for the same reason: an entry (in particular a cached failure) computed under an + erasure must not be served once the surrounding scope ends and restores the instance. + -/ + erasedInsts : Array Name + /-- Effective maximum result size (`synthInstance.maxSize` unless overridden by the caller). The cache persists across commands, so results (in particular failures) obtained under a different size limit must not be reused. @@ -409,6 +429,11 @@ structure SynthInstanceCacheKey where -/ defEqFlags : SynthDefEqFlags /-- + Value of `Environment.isExporting`: in the exporting state, fewer definitions can be unfolded, + which can change the result of typeclass resolution. + -/ + isExporting : Bool + /-- The resource limits in effect for the query (`maxHeartbeats`, `synthInstance.maxHeartbeats`, `maxRecDepth`, `exponentiation.threshold`). Exceeding a limit throws, and results are only cached on the success path, so a limit cannot influence a stored result; keying by them @@ -786,9 +811,6 @@ def mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey := @[inline] def resetDefEqPermCaches : MetaM Unit := modifyDefEqPermCache fun _ => {} -@[inline] def resetSynthInstanceCache : MetaM Unit := - modifyCache fun c => {c with synthInstance := {}} - @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do if (← isDiagnosticsEnabled) then modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag } diff --git a/src/Lean/Meta/Constructions/SparseCasesOn.lean b/src/Lean/Meta/Constructions/SparseCasesOn.lean index f184572b0c27..146a1406b892 100644 --- a/src/Lean/Meta/Constructions/SparseCasesOn.lean +++ b/src/Lean/Meta/Constructions/SparseCasesOn.lean @@ -24,7 +24,10 @@ structure SparseCasesOnKey where deriving BEq, Hashable builtin_initialize sparseCasesOnCacheExt : EnvExtension (PHashMap SparseCasesOnKey Name) ← - registerEnvExtension (pure {}) (asyncMode := .local) -- mere cache, keep it local + -- mere cache, keep it local; may be consulted on resolution search paths via the reserved-name + -- covered: realization cache, populated on demand; reads never observe result-relevant + -- absence, and entries are write-stability-guarded + registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true) /-- Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs) -/ public structure SparseCasesOnInfo where @@ -35,6 +38,8 @@ public structure SparseCasesOnInfo where deriving Inhabited builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnInfo ← + -- consulted by the reserved-name predicate for `else_eq` names, so also on resolution search + -- paths; populated only when the declaration is created (monotone) mkMapDeclarationExtension (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels @@ -133,7 +138,15 @@ public def mkSparseCasesOn (indName : Name) (ctors : Array Name) : MetaM Name := (value := value) (hints := ReducibilityHints.abbrev) addDecl (.defnDecl decl) - modifyEnv fun env => sparseCasesOnCacheExt.modifyState env fun s => s.insert key declName + modifyEnv fun env => sparseCasesOnCacheExt.modifyState env fun s => + -- write-stability guard; see `MapDeclarationExtension.insert` + match s.find? key with + | some prev => + if prev != declName then + panic! s!"sparse `casesOn` for `{declName}` is already registered as `{prev}`" + else + s + | none => s.insert key declName setReducibleAttribute declName modifyEnv fun env => markSparseCasesOn env declName modifyEnv fun env => sparseCasesOnInfoExt.insert env declName { diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index c20d482ac376..b323c2b24bbd 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -47,6 +47,8 @@ def eqnAffectingOptions : Array (Lean.Option Bool) := keyed by declaration name. Only populated when at least one option has a non-default value. Stores an association list of (option name, value) pairs for options that differ from defaults. -/ builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ← + -- consulted during equation realization, which can happen inside a resolution search; + -- populated only when the declaration is created (monotone) mkMapDeclarationExtension (asyncMode := .local) def eqnThmSuffixBase := "eq" @@ -157,7 +159,10 @@ structure EqnsExtState where /-- A mapping from equational theorem to the declaration it was derived from. -/ builtin_initialize eqnsExt : EnvExtension EqnsExtState ← - registerEnvExtension (pure {}) (asyncMode := .local) + -- consulted during equation realization, which can happen inside a resolution search; + -- covered: realized on demand, so reads never observe result-relevant absence, and + -- registered equations are write-stability-guarded + registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true) /-- Runs `act` with the equation-affecting options restored to the values stored for `declName` @@ -216,7 +221,16 @@ Stores in the `eqnsExt` environment extension that `eqThms` are the equational t -/ private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit := do modifyEnv fun env => eqnsExt.modifyState env fun s => { s with - mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => mapInv.insert eqThm declName + mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => + -- write-stability guard; see `MapDeclarationExtension.insert`. Re-registration with the + -- same parent is idempotent (e.g. `alreadyGenerated?` re-registers realized equations). + match mapInv.find? eqThm with + | some prev => + if prev != declName then + panic! s!"equation theorem `{eqThm}` is already registered for `{prev}`" + else + mapInv + | none => mapInv.insert eqThm declName } /-- diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 98ed55bb22bb..8423864cdead 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -77,15 +77,28 @@ structure Instances where discrTree : InstanceTree := DiscrTree.empty instanceNames : PHashMap Name InstanceEntry := {} erased : PHashSet Name := {} + /-- + Names of instances added with the `local` attribute kind into this state, in insertion order. + Local instances are delimited by their surrounding scope, which restores the previous + `Instances` state (and thereby the previous value of this field) when it is closed. The field + is part of the type class resolution cache key (`SynthInstanceCacheKey.localAttrInsts`), so + cache entries never leak into or out of scopes with local instances. + -/ + localInstanceNames : Array Name := #[] deriving Inhabited def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances := + let d := if e.attrKind matches .local then + { d with localInstanceNames := d.localInstanceNames.push (e.globalName?.getD .anonymous) } + else + d match e.globalName? with | some n => { d with discrTree := d.discrTree.insertKeyValue e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n } | none => { d with discrTree := d.discrTree.insertKeyValue e.keys e } def Instances.eraseCore (d : Instances) (declName : Name) : Instances := - { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName } + { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName, + localInstanceNames := d.localInstanceNames.filter (· != declName) } def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do unless d.instanceNames.contains declName do @@ -99,8 +112,25 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In exportEntry? := fun _ e => if e.globalName?.any (!isPrivateName ·) then .uniform (some e) else ⟨none, none, some e⟩ + -- adding or erasing an instance bumps the generation, invalidating resolution cache + -- entries that consulted the instance table; scope activation is covered by the cache key + -- (`SynthInstanceCacheKey.activeScopedInsts`/`localAttrInsts`) instead + trackGen := true } +/-- +Resets the type class resolution cache (`Meta.Cache.synthInstance`). + +Calling this function is normally unnecessary: cache entries record the dependencies of their +search (relevant options, instances, unification hints, reducibility statuses; see +`Lean.Meta.SynthInstance`) and are automatically invalidated when a dependency changes. Known +remaining gaps that do require an explicit reset: deactivation of *scoped* unification hints +(ending the surrounding scope or section), and dropping *local* unification hints at the end of +a section, neither of which is covered by the cache key or the recorded dependencies. +-/ +def resetSynthInstanceCache : MetaM Unit := do + modifyCache fun c => { c with synthInstance := {} } + private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do let type ← inferType e withNewMCtxDepth do @@ -353,24 +383,28 @@ builtin_initialize modifyEnv fun env => instanceExtension.modifyState env fun _ => s } +-- `recorded := true` below: every resolution query records the instance-table generation once +-- when it starts (`Lean.recordExtGenAccess` in `synthInstanceCore?`), which covers every +-- read of the table during the query. + def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) := - return Meta.instanceExtension.getState (← getEnv) |>.discrTree + return Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.discrTree def getErasedInstances : CoreM (PHashSet Name) := - return Meta.instanceExtension.getState (← getEnv) |>.erased + return Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.erased def isInstanceCore (env : Environment) (declName : Name) : Bool := - Meta.instanceExtension.getState env |>.instanceNames.contains declName + Meta.instanceExtension.getState (recorded := true) env |>.instanceNames.contains declName def isInstance (declName : Name) : CoreM Bool := return isInstanceCore (← getEnv) declName def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do - let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none + let some entry := Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.instanceNames.find? declName | return none return entry.priority def getInstanceAttrKind? (declName : Name) : CoreM (Option AttributeKind) := do - let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none + let some entry := Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.instanceNames.find? declName | return none return entry.attrKind /-! # Default instance support -/ diff --git a/src/Lean/Meta/Match/MatchEqsExt.lean b/src/Lean/Meta/Match/MatchEqsExt.lean index 07d1f07a1611..9212ebec0028 100644 --- a/src/Lean/Meta/Match/MatchEqsExt.lean +++ b/src/Lean/Meta/Match/MatchEqsExt.lean @@ -30,15 +30,27 @@ structure MatchEqnsExtState where /- We generate the equations and splitter on demand, and do not save them on .olean files. -/ builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ← + -- consulted during match-equation realization, which can happen inside a resolution search; + -- a mere name mapping for realized equation theorems (monotone) -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`. -- The resulting state can still be accessed on the generated declarations using `.asyncEnv`; - -- see below - registerEnvExtension (pure {}) (asyncMode := .local) + -- see below. Covered: realized on demand, so reads never observe result-relevant absence, + -- and registered equations are write-stability-guarded. + registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true) def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit := do modifyEnv fun env => matchEqnsExt.modifyState env fun { map, eqns } => { eqns := matchEqns.eqnNames.foldl (init := eqns) fun eqns eqn => eqns.insert eqn - map := map.insert matchDeclName matchEqns + -- write-stability guard; see `MapDeclarationExtension.insert`. Re-registration with the + -- same equations is idempotent. + map := + match map.find? matchDeclName with + | some prev => + if prev.eqnNames != matchEqns.eqnNames then + panic! s!"match equations for `{matchDeclName}` are already registered" + else + map + | none => map.insert matchDeclName matchEqns } /- diff --git a/src/Lean/Meta/Match/MatchPatternAttr.lean b/src/Lean/Meta/Match/MatchPatternAttr.lean index d7e0883c6a4a..e9d12ce671e1 100644 --- a/src/Lean/Meta/Match/MatchPatternAttr.lean +++ b/src/Lean/Meta/Match/MatchPatternAttr.lean @@ -32,7 +32,10 @@ def isYellow (color : String) : Bool := -/ @[builtin_doc] builtin_initialize matchPatternAttr : TagAttribute ← - registerTagAttribute `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)" + -- consulted during resolution `isDefEq`; post-hoc tagging is treated as decl-time (the tag is + -- effectively part of the definition) + -- covered: declaration-keyed; post-hoc applications are recorded in the declaration change log + registerTagAttribute (declCovered := true) `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)" (validate := fun declName => do withExporting (isExporting := !isPrivateName declName) do if !(← getConstInfo declName).isDefinition then diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index b1f76d269f21..be4268b16270 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -127,6 +127,8 @@ builtin_initialize extension : SimplePersistentEnvExtension Entry State ← addEntryFn := State.addEntry addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch asyncMode := .async .mainEnv + -- covered: matcher facts are immutable per declaration and monotone + declCovered := true exportEntriesFnEx? := some fun env _ entries => let all := entries.toArray -- Do not export info for private defs at exported/server levels diff --git a/src/Lean/Meta/MethodSpecs.lean b/src/Lean/Meta/MethodSpecs.lean index b5a044e7073f..6702ea683237 100644 --- a/src/Lean/Meta/MethodSpecs.lean +++ b/src/Lean/Meta/MethodSpecs.lean @@ -112,12 +112,20 @@ overloaded `Cls.op` operation, and similarly `instClsT.op_spec_` based on the `opImpl.eq_`. -/ @[builtin_doc] -builtin_initialize methodSpecsAttr : ParametricAttribute MethodSpecsAttrData ← - registerParametricAttribute { +builtin_initialize methodSpecsAttr : ParametricAttribute MethodSpecsAttrData ← do + let impl : ParametricAttributeImpl MethodSpecsAttrData := { name := `method_specs descr := "generate method specification theorems" getParam } + -- consulted (via the reserved-name machinery) when specification theorems are realized, which + -- can happen inside a resolution search; the attribute is applied when the method + -- implementation is declared (monotone) + -- covered: declaration-keyed, applied when the method implementation is declared + let ext ← registerParametricAttributeExt (α := MethodSpecsAttrData) impl.ref impl.preserveOrder + (declCovered := true) + impl.filterExport + registerParametricAttributeForExt impl ext builtin_initialize methodSpecsSimpExtension : SimpExtension ← registerSimpAttr `method_specs_simp diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index c3bae2912411..23c6204a2747 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -32,6 +32,11 @@ register_builtin_option backward.synthInstance.canonInstances : Bool := { descr := "use optimization that relies on 'morally canonical' instances during type class resolution" } +register_builtin_option debug.synthInstance.checkCacheHits : Bool := { + defValue := false + descr := "differentially validate type class resolution cache hits: re-run every served query from scratch and panic if the recomputed result differs from the cached one, which means a dependency of the entry was not recorded (development soak check; roughly doubles resolution cost)" +} + namespace SynthInstance def getMaxHeartbeats (opts : Options) : Nat := @@ -928,21 +933,28 @@ private def validOptionAccesses (opts : Options) (log : SynthOptionAccessLog) : log.all fun a => opts.find? a.name == a.value /-- -Merges the dependencies observed by a nested query (or served from a used cache entry) into the -enclosing query's accumulator: the enclosing query observed the nested result, so it depends on -whatever the nested one did. +Merges the environment dependencies observed by a nested query (or served from a used cache +entry) into the enclosing query's accumulator. The enclosing query keeps its own +`changeLogPos` and `recordGen`: they were captured when that query started, and the merged +dependencies are validated against them like the query's own observations. -/ private def _root_.Lean.RecordedDeps.mergeInto (child parent : RecordedDeps) : RecordedDeps := let options := child.options.foldl (init := parent.options) fun l a => if l.any (·.name == a.name) then l else l.push a - { parent with options } + let extGens := child.extGens.foldl (init := parent.extGens) fun l d => + if l.any (·.1 == d.1) then l else l.push d + { parent with options, extGens } /-- -Identity of two dependency logs for entry replacement in `insertCachedResult`: the same option -lookups with the same answers. +Identity of two dependency logs for entry replacement in `insertCachedResult`: same option +answers and same dependency *shape* (same extensions and reducibility declarations observed). +The observed generations and statuses are deliberately not part of the identity: a fresh +observation with the same shape supersedes the old entry, whose generations can never recur. -/ private def sameDepIdentity (a b : RecordedDeps) : Bool := a.options == b.options + && a.extGens.size == b.extGens.size + && a.extGens.all (fun d => b.extGens.any (·.1 == d.1)) /-- Inserts a result into the type class resolution cache (`Meta.Cache.synthInstance`), which has @@ -958,13 +970,30 @@ private def insertCachedResult (key : SynthInstanceCacheKey) (log : RecordedDeps modifyCache fun c => { c with synthInstance := upsert c.synthInstance } /-- -Validates a cache entry's recorded dependencies against the current context: every recorded -option lookup must give the same answer. Returns `none` if the entry may not be used. +Validates a cache entry's recorded dependencies against the current context. Returns `none` if +any recorded answer has changed; otherwise the entry may be used, and the returned Boolean +indicates the log was *re-stamped*: `Environment.recordGen` had moved, all recorded +dependencies re-answered identically, and the log now carries the current stamps (including +the reducibility log position and birth watermark, so each log segment is scanned at most once +per entry). The caller re-inserts a re-stamped entry. + +The status re-asks may record into the armed query's accumulator, which is benign: it +over-approximates the current query's dependencies. -/ -private def validateDeps? (opts : Options) (_env : Environment) +private def validateDeps? (opts : Options) (env : Environment) (log : RecordedDeps) : BaseIO (Option (RecordedDeps × Bool)) := do unless validOptionAccesses opts log.options do return none - return some (log, false) + -- Global short-circuit: while `Environment.recordGen` is unchanged, no recorded environment + -- dependency can have changed and the per-dependency checks are skipped. + if log.recordGen == env.recordGen then + return some (log, false) + for (idx, gen) in log.extGens do + unless (← EnvExtension.getRecordedGen env idx) == gen do return none + unless env.checkDeclChangeLog log.changeLogPos log.constBirthW do return none + return some ({ log with + recordGen := env.recordGen + changeLogPos := env.declChangeLog.size + constBirthW := env.constBirthGen }, true) /-- Returns the type class resolution cache entry for `key` from the transient @@ -1034,6 +1063,13 @@ private def synthInstanceConfig : Config := { isDefEqStuckEx := true, transparency := .instances, foApprox := true, ctxApprox := true, constApprox := false, univApprox := false } +/-- +Marks the query as recording on the environment (`Environment.isRecordingDeps`) without +resetting `Meta.Cache` (which `Meta.modifyEnv` would). +-/ +private def setRecordingDeps (recording : Bool) : MetaM Unit := + modifyThe Core.State fun s => { s with env := s.env.setRecordingDeps recording } + def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do -- For a nested query this read happens under the enclosing query's restriction and is recorded -- as its dependency: the value determines the nested query's cache key. @@ -1041,17 +1077,23 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met | some n => pure n | none => getRecordedOption synthInstance.maxSize -- The query's dependencies: result-relevant option lookups on the search path go through the - -- recording accessors (`getRecordedOption`) and flow into the accumulator - -- `Core.State.recordedDeps`, which becomes the cache entry's dependency log, see - -- `SynthInstanceCache`. The enclosing query's accumulator (if any) is saved here and the - -- nested query's effective dependencies are merged into it on exit (`finally` below): the - -- enclosing query observed the result. + -- recording accessors (`getRecordedOption`), and observed environment dependencies are + -- recorded directly; both flow into the accumulator `Core.State.recordedDeps`, which becomes + -- the cache entry's dependency log, see `SynthInstanceCache`. The enclosing query's + -- accumulator (if any) is saved here and the nested query's effective dependencies are + -- merged into it on exit (`finally` below): the enclosing query observed the result. let parentDeps := (← getThe Core.State).recordedDeps let parentRecording := (← readThe Core.Context).recordingDeps - modifyThe Core.State fun s => { s with recordedDeps := {} } + let fresh : RecordedDeps := + { recordGen := (← getEnv).recordGen + changeLogPos := (← getEnv).declChangeLog.size + constBirthW := (← getEnv).constBirthGen } + modifyThe Core.State fun s => { s with recordedDeps := fresh } + -- Both halves of the recording marker are armed here and must stay in lockstep: pure + -- extension reads can only see the one on the environment (`EnvExtension.trackGen`), while + -- everything reading through `CoreM` sees the scoped one, which needs no restoring. + setRecordingDeps true try - -- Mark the query as recording; the marker is scoped to the search, so only the accumulator - -- has to be restored below. withTheReader Core.Context (fun ctx => { ctx with recordingDeps := true }) do -- Resolve the per-step definitional-equality flags once; they are part of the cache key -- rather than recorded dependencies, so the raw reads are not logged. See `SynthDefEqFlags`. @@ -1088,8 +1130,17 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met let localInsts ← getLocalInstances let type ← instantiateMVars type let { type, cacheKeyType, kind } ← preprocess type + -- The instance-table generation is recorded once per query here, covering every read of + -- the table on the search path. + recordExtGenAccess instanceExtension.ext.toEnvExtension.idx + let insts := instanceExtension.getState (recorded := true) (← getEnv) let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth, - maxResultSize, defEqFlags := flags, limits } + activeScopedInsts := instanceExtension.getActiveScopesWithEntries (recorded := true) (← getEnv), + localAttrInsts := insts.localInstanceNames, + erasedInsts := if insts.erased.isEmpty then #[] + else insts.erased.fold (init := #[]) (·.push ·) |>.qsort Name.quickLt, + maxResultSize, defEqFlags := flags, limits, + isExporting := (← getEnv).isExporting } let runSearch : MetaM (Option AbstractMVarsResult) := withNewMCtxDepth (allowLevelAssignments := true) do match kind with @@ -1116,11 +1167,47 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met SynthInstance.main (← preprocessOutParam type) maxResultSize | .mvarsNoOutputParams => SynthInstance.main type maxResultSize | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize + -- Differential validation of a served hit (`debug.synthInstance.checkCacheHits`): recompute + -- the query from scratch and compare against the served result. The recompute bypasses the + -- entry under test by construction (the search body performs no cache lookup), and its + -- recorded dependencies flow into the current accumulator, which only strengthens the + -- entry's log. Raw `toString` is used for reporting: the pretty printer acquires the options, + -- which the recording marker diverts. + let checkHit (served? : Option AbstractMVarsResult) : MetaM Unit := do + -- deliberately unrestricted acquisition: purely diagnostic, cannot influence a cached result + unless debug.synthInstance.checkCacheHits.get (← getOptionsUnrestricted) do return + -- Fresh heartbeat budget: the recompute must not consume the query's own allowance. The + -- check is observation-only, so recompute exceptions are reported instead of propagated: + -- a search that throws where the cache had an answer is itself a divergence. + let fresh?? : Except String (Option AbstractMVarsResult) ← + try + .ok <$> withCurrHeartbeats runSearch + catch ex => do + let msg ← ex.toMessageData.toString + pure <| .error s!"exception: {msg}" + let pp : Option AbstractMVarsResult → String + | none => "none" + | some r => toString r.expr + let mismatch? : Option String := match fresh?? with + | .error e => some e + | .ok fresh? => + let same := match served?, fresh? with + | none, none => true + | some a, some b => a.numMVars == b.numMVars && a.paramNames == b.paramNames && a.expr == b.expr + | _, _ => false + if same then none else some (pp fresh?) + if let some fresh := mismatch? then + -- the panic is the branch result: an unused pure binding would be dead-code-eliminated + panic! s!"type class resolution cache hit differs from recomputation for\n \ + {toString type}\ncached: {pp served?}\nrecomputed: {fresh}\n\ + an environment dependency of the served entry was not recorded; see \ + `Lean.EnvExtension.trackGen`" match ← findCachedResult? cacheKey with | some (entryLog, abstResult?) => trace[Meta.synthInstance.cache] "cached: {type}" -- The used entry's dependencies become dependencies of this query. - modifyThe Core.State fun s => { s with recordedDeps := entryLog.mergeInto s.recordedDeps } + Core.modifyRecordedDeps entryLog.mergeInto + checkHit abstResult? let result? ← applyCachedAbstractResult? type abstResult? trace[Meta.synthInstance] "result {result?} (cached)" return result? @@ -1133,7 +1220,9 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met return result? finally -- Restore the enclosing accumulator, merging this query's effective dependencies into it. + -- The environment half of the marker is state, so unlike the scoped half it is restored here. let childDeps := (← getThe Core.State).recordedDeps + setRecordingDeps parentRecording modifyThe Core.State fun s => { s with recordedDeps := if parentRecording then childDeps.mergeInto parentDeps else parentDeps } diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean index b4a6bbf8add0..f0150ac4e4b7 100644 --- a/src/Lean/Meta/UnificationHint.lean +++ b/src/Lean/Meta/UnificationHint.lean @@ -38,6 +38,10 @@ builtin_initialize unificationHintExtension : SimpleScopedEnvExtension Unificati registerSimpleScopedEnvExtension { addEntry := UnificationHints.add initial := {} + -- adding a hint bumps the generation, invalidating resolution cache entries that consulted + -- the hints; unlike reducibility there is no declaration-time exemption, as a new hint + -- applies to pre-existing terms + trackGen := true } structure UnificationConstraint where @@ -102,7 +106,8 @@ def tryUnificationHints (t s : Expr) : MetaM Bool := do return false if t.isMVar then return false - let hints := unificationHintExtension.getState (← getEnv) + recordExtGenAccess unificationHintExtension.ext.toEnvExtension.idx + let hints := unificationHintExtension.getState (recorded := true) (← getEnv) let candidates ← withConfigWithKey config <| hints.discrTree.getMatch t for candidate in candidates do if (← tryCandidate candidate) then diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean index f58c99d0dec0..39d7b7895bbb 100644 --- a/src/Lean/ProjFns.lean +++ b/src/Lean/ProjFns.lean @@ -27,7 +27,9 @@ structure ProjectionFunctionInfo where fromClass : Bool deriving Inhabited, Repr -builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension +builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← + -- covered: projection facts are immutable per declaration and monotone + mkMapDeclarationExtension (declCovered := true) def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment := projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass } @@ -70,7 +72,9 @@ structure AuxParentProjectionInfo where fromClass : Bool deriving Inhabited, Repr -builtin_initialize auxParentProjInfoExt : MapDeclarationExtension AuxParentProjectionInfo ← mkMapDeclarationExtension +builtin_initialize auxParentProjInfoExt : MapDeclarationExtension AuxParentProjectionInfo ← + -- covered: parent-projection facts are immutable per declaration and monotone + mkMapDeclarationExtension (declCovered := true) def addAuxParentProjectionInfo (env : Environment) (projName : Name) (numParams : Nat) (fromClass : Bool) : Environment := auxParentProjInfoExt.insert env projName { numParams, fromClass } diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index d32f8582486f..73e5839d6b9e 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -51,6 +51,9 @@ def ReducibilityStatus.toAttrString : ReducibilityStatus → String builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ← registerPersistentEnvExtension { name := `reducibilityCore + -- covered: status changes about observable declarations are recorded in the declaration + -- change log and validated by birth arithmetic (see `Environment.declChangeLog`) + declCovered := true mkInitial := pure {} addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2 @@ -71,6 +74,8 @@ builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × Reducib builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ← registerSimpleScopedEnvExtension { name := `reducibilityExtra + -- covered: as for `reducibilityCoreExt` above + declCovered := true initial := {} addEntry := fun d (declName, status) => d.insert declName status finalizeImport := fun d => d.switch @@ -101,22 +106,14 @@ private def setReducibilityStatusCore (env : Environment) (declName : Name) (sta reducibilityExtraExt.addCore env (declName, status) attrKind currNamespace /- -TODO: it would be great if we could distinguish between the following two situations - -1- -``` -@[reducible] def foo := ... -``` - -2- -``` -def foo := ... -... -attribute [reducible] foo -``` - -Reason: the second one is problematic if user has add simp theorems or TC instances that include `foo`. -Recall that the discrimination trees unfold `[reducible]` declarations while indexing new entries. +The type class resolution cache distinguishes the following two situations by birth arithmetic +(`Environment.declChangeLog`): an attribute that is part of `foo`'s own elaboration +(`@[reducible] def foo := ...`) is skipped during validation, while a post-hoc +`attribute [reducible] foo` invalidates the entries that could have observed the old status. + +TODO: the distinction is not yet surfaced to other consumers: discrimination trees unfold +`[reducible]` declarations while indexing new entries, so a post-hoc change can invalidate +already-indexed simp theorems or TC instances mentioning `foo`; see `validate` below. -/ register_builtin_option allowUnsafeReducibility : Bool := { @@ -182,6 +179,9 @@ private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Synta validate declName status attrKind let ns ← getCurrNamespace modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns + -- Reducibility determines what `isDefEq` may unfold, so a status change some recording + -- query could have observed must be recorded; see `Environment.declChangeLog`. + modifyEnv fun env => env.logDeclChange declName builtin_initialize registerBuiltinAttribute { @@ -256,7 +256,13 @@ builtin_initialize def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do return getReducibilityStatusCore (← getEnv) declName -/-- Set the reducibility attribute for the given declaration. -/ +/-- +Set the reducibility attribute for the given declaration. + +Note: does not bump the reducibility change counter (`reducibilityChangedExt`). Use only for +declarations created by the caller itself (before other code can have cached results about +them); status changes to pre-existing declarations must go through the reducibility attributes. +-/ def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index b687cc6b3cb7..d101461cd986 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -43,7 +43,9 @@ def registerReservedNamePredicate (p : Environment → Name → Bool) : IO Unit reservedNamePredicatesRef.modify fun ps => ps.push p builtin_initialize reservedNamePredicatesExt : EnvExtension (Array (Environment → Name → Bool)) ← - registerEnvExtension reservedNamePredicatesRef.get + -- covered: consulted by `Environment.find?` (via `isReservedName`), so also on resolution + -- search paths; the predicate set is fixed at initialization + registerEnvExtension reservedNamePredicatesRef.get (declCovered := true) /-- Returns `true` if `name` is a reserved name. diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean index 69a91dfc305b..0704b401aa94 100644 --- a/src/Lean/ScopedEnvExtension.lean +++ b/src/Lean/ScopedEnvExtension.lean @@ -40,6 +40,10 @@ structure Descr (α : Type) (β : Type) (σ : Type) where addEntry : σ → β → σ finalizeImport : σ → σ := id exportEntry? : Environment → α → OLeanEntries (Option α) := fun _ a => .uniform (some a) + /-- See `EnvExtension.trackGen`. -/ + trackGen : Bool := false + /-- See `EnvExtension.trackGen`. -/ + declCovered : Bool := false instance [Inhabited α] : Inhabited (Descr α β σ) where default := { @@ -135,6 +139,8 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope -- `AsyncMode.local` below). Allowing the latter is important for tactics such as -- `classical` -- or `open in`. asyncMode := .mainOnly + trackGen := descr.trackGen + declCovered := descr.declCovered } let ext := { descr := descr, ext := ext : ScopedEnvExtension α β σ } scopedEnvExtensionsRef.modify fun exts => exts.push (unsafeCast ext) @@ -143,14 +149,22 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope @[implemented_by registerScopedEnvExtensionUnsafe] opaque registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ) +/- +The scope-stack operations (`pushScope`/`popScope`/`setDelimitsLocal`/`activateScoped`) preserve +the generation of `.recorded` extensions (`keepRecordGen`): for the type class resolution cache, +scope activation state is part of the cache key (`SynthInstanceCacheKey.activeScopedInsts`), +and entries computed with local entries in scope are keyed or documented as requiring an +explicit reset (see `Lean.Meta.resetSynthInstanceCache`). Content changes (`addEntry` and +friends) bump the generation as usual. +-/ def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment := - ext.ext.modifyState (asyncMode := .local) env fun s => + ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s => match s.stateStack with | [] => s | state :: stack => { s with stateStack := { state with delimitsLocal := true } :: state :: stack } def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment := - ext.ext.modifyState (asyncMode := .local) env fun s => + ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s => match s.stateStack with | _ :: state₂ :: stack => { s with stateStack := state₂ :: stack } | _ => s @@ -160,7 +174,7 @@ to turn off delimiting of local entries across multiple implicit scope levels (e.g. those introduced by compound `namespace A.B.C` expansions). -/ def ScopedEnvExtension.setDelimitsLocal (ext : ScopedEnvExtension α β σ) (env : Environment) (depth : Nat) : Environment := - ext.ext.modifyState (asyncMode := .local) env fun s => + ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s => {s with stateStack := go depth s.stateStack} where go : Nat → List (State σ) → List (State σ) @@ -203,13 +217,28 @@ def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : Sc modifyEnv (ext.addCore · b kind ns) def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) - (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode) : σ := - match ext.ext.getState (asyncMode := asyncMode) env |>.stateStack with + (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode) + (recorded := false) : σ := + match ext.ext.getState (asyncMode := asyncMode) (recorded := recorded) env |>.stateStack with | top :: _ => top.state | _ => unreachable! +/-- +Returns the active scopes of `ext` that have scoped entries, in a canonical order. Activated +namespaces without scoped entries for this extension are omitted, so the result only changes when +the set of activated scoped entries may have changed. +-/ +def ScopedEnvExtension.getActiveScopesWithEntries (ext : ScopedEnvExtension α β σ) + (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode) + (recorded := false) : Array Name := + let s := ext.ext.getState (asyncMode := asyncMode) (recorded := recorded) env + match s.stateStack with + | top :: _ => top.activeScopes.foldl (init := #[]) fun acc ns => + if s.scopedEntries.map.contains ns then acc.push ns else acc + | _ => #[] + def ScopedEnvExtension.activateScoped (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) : Environment := - ext.ext.modifyState (asyncMode := .local) env fun s => + ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s => match s.stateStack with | top :: stack => if top.activeScopes.contains namespaceName then @@ -261,6 +290,10 @@ structure SimpleScopedEnvExtension.Descr (α : Type) (σ : Type) where initial : σ finalizeImport : σ → σ := id exportEntry? : Environment → α → OLeanEntries (Option α) := fun _ a => .uniform (some a) + /-- See `EnvExtension.trackGen`. -/ + trackGen : Bool := false + /-- See `EnvExtension.trackGen`. -/ + declCovered : Bool := false def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α σ) : IO (SimpleScopedEnvExtension α σ) := do registerScopedEnvExtension { @@ -271,6 +304,8 @@ def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α ofOLeanEntry := fun _ a => return a finalizeImport := descr.finalizeImport exportEntry? := descr.exportEntry? + trackGen := descr.trackGen + declCovered := descr.declCovered } end Lean diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 77e580c4e57b..066d85c80660 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -85,6 +85,9 @@ private structure StructureState where deriving Inhabited private builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension { + -- covered: structure facts are immutable per declaration (the sanctioned `parentInfo` update + -- in `setStructureParents` is recorded in the declaration change log) + declCovered := true mkInitial := pure ((), {}) addImportedFn := fun _ => pure ((), {}) addEntryFn := fun (_, s) e => ((), { s with map := s.map.insert e.structName e }) @@ -107,11 +110,17 @@ Every structure created by `structure` or `class` has such an entry. This should be followed up with `setStructureParents` and `setStructureResolutionOrder`. -/ def registerStructure (env : Environment) (e : StructureDescr) : Environment := - structureExt.addEntry env { - structName := e.structName - fieldNames := e.fields.map fun e => e.fieldName - fieldInfo := e.fields.qsort StructureFieldInfo.lt - } + have : Inhabited Environment := ⟨env⟩ + -- Write-once guard; see `MapDeclarationExtension.insert`. The one sanctioned update is + -- `setStructureParents` below. + if structureExt.getState env |>.snd.map.contains e.structName then + panic! s!"structure `{e.structName}` is already registered" + else + structureExt.addEntry env { + structName := e.structName + fieldNames := e.fields.map fun e => e.fieldName + fieldInfo := e.fields.qsort StructureFieldInfo.lt + } /-- Sets parent projection info for a structure defined in the current module. @@ -120,7 +129,11 @@ Throws an error if the structure has not already been registered with `Lean.regi def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name) (parentInfo : Array StructureParentInfo) : m Unit := do let some info := structureExt.getState (← getEnv) |>.snd.map.find? structName | throwError "cannot set structure parents for `{structName}`, structure not defined in current module" - modifyEnv fun env => structureExt.addEntry env { info with parentInfo } + -- Sanctioned second write to the structure's entry: `parentInfo` is filled in after + -- `registerStructure`, once the parent projections exist. The change is recorded in the + -- declaration change log, so entries armed in between (e.g. from default-value elaboration) + -- are invalidated by birth arithmetic; see `Environment.declChangeLog`. + modifyEnv fun env => structureExt.addEntry (env.logDeclChange structName) { info with parentInfo } /-- Gets the `StructureInfo` if `structName` has been declared as a structure to the elaborator. -/ def getStructureInfo? (env : Environment) (structName : Name) : Option StructureInfo := @@ -419,7 +432,8 @@ We use an environment extension to cache resolution orders. These are not expensive to compute, but worth caching, and we save olean storage space. -/ builtin_initialize structureResolutionExt : EnvExtension StructureResolutionState ← - registerEnvExtension (pure {}) (asyncMode := .local) -- mere cache + -- covered: mere cache of a pure computation over covered inputs + registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true) /-- Gets the resolution order if it has already been cached. -/ private def getStructureResolutionOrder? (env : Environment) (structName : Name) : Option (Array Name) := diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index 51fe5793e2c1..50cf529ac06b 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -64,9 +64,19 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ← } builtin_initialize ppExt : EnvExtension PPFns ← - registerEnvExtension ppFnsRef.get + registerEnvExtension ppFnsRef.get (name := `pp) + +/-- +Pretty printing is a legitimate consumer of arbitrary extension state even when its context was +captured inside a region with restricted extension access (e.g. a trace message constructed +during type class resolution): rendering happens outside the restricted computation and cannot +contaminate its caches. Lift the restriction from the captured environment. +-/ +private def PPContext.unrestricted (ctx : PPContext) : PPContext := + { ctx with env := ctx.env.setRecordingDeps false } def ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos := do + let ctx := ctx.unrestricted if pp.raw.get ctx.opts then let e := instantiateMVarsCore ctx.mctx e |>.1 return format (toString e) @@ -80,6 +90,7 @@ def ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos := do pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)" def ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos := do + let ctx := ctx.unrestricted match (← ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n |>.toBaseIO) with | .ok fmt => return fmt | .error ex => @@ -89,6 +100,7 @@ def ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos : pure f!"failed to pretty print constant (use 'set_option pp.rawOnError true' for raw representation)" def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do + let ctx := ctx.unrestricted if pp.raw.get ctx.opts then return formatRawTerm ctx stx else @@ -101,6 +113,7 @@ def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)" def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format := do + let ctx := ctx.unrestricted match (← ppExt.getState ctx.env |>.ppLevel ctx l |>.toBaseIO) with | .ok fmt => return fmt | .error ex => @@ -110,6 +123,7 @@ def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format := do pure f!"failed to pretty print level (use 'set_option pp.rawOnError true' for raw representation)" def ppGoal (ctx : PPContext) (mvarId : MVarId) : BaseIO Format := do + let ctx := ctx.unrestricted match (← ppExt.getState ctx.env |>.ppGoal ctx mvarId |>.toBaseIO) with | .ok fmt => return fmt | .error ex => diff --git a/tests/elab/tc_cache_check_hits.lean b/tests/elab/tc_cache_check_hits.lean new file mode 100644 index 000000000000..5d1b4c861263 --- /dev/null +++ b/tests/elab/tc_cache_check_hits.lean @@ -0,0 +1,34 @@ +/-! +Runs representative elaboration with `debug.synthInstance.checkCacheHits`, the differential +validation of type class resolution cache hits: every served entry is recomputed from scratch +and compared. A panic here means a served result diverged from recomputation, i.e. some +dependency of the entry was not recorded. +-/ + +set_option debug.synthInstance.checkCacheHits true + +class R (α : Type) where + val : Nat + +instance : R Nat := ⟨1⟩ +instance : R (List α) := ⟨2⟩ +instance [R α] [R β] : R (α × β) := ⟨3⟩ + +def f (n : Nat) : Nat := R.val Nat + n + +example : R.val (List Nat) = 2 := rfl +example : R.val (List Nat) = 2 := rfl +example : R.val (Nat × List Nat) = 3 := rfl +example : R.val (Nat × List Nat) = 3 := rfl + +def sumIt (l : List Nat) : Nat := l.foldl (· + ·) 0 + +example : sumIt [1, 2, 3] = 6 := by simp [sumIt] +example : sumIt [1, 2, 3] = 6 := by simp [sumIt] + +structure Wrap where + out : Nat + +instance : R Wrap := ⟨4⟩ + +example (w : Wrap) : R.val Wrap + w.out = 4 + w.out := rfl diff --git a/tests/elab/tc_cache_covered_claims.lean b/tests/elab/tc_cache_covered_claims.lean new file mode 100644 index 000000000000..2434a9acbafc --- /dev/null +++ b/tests/elab/tc_cache_covered_claims.lean @@ -0,0 +1,76 @@ +/-! +Locks the extension-classification audit of the type class resolution dependency tracking: any +resolution-path read of an unclassified environment extension panics unconditionally (see +`Lean.EnvExtension.trackGen`). The file elaborates representative content whose searches +traverse the covered extensions: structures and classes (structure info, class table, +projection functions), instances with out-params, matchers and equation realization (matcher +info, eqns, match eqns), reducibility reads and post-hoc changes (declaration change log), and +auxiliary recursors. A panic here means the search path reached an extension that should +either be registered as covered (`declCovered`, with a justification) or generation-tracked +and read through the recording accessors. +-/ + +structure Pt where + x : Nat + y : Nat + +class Dist (α : Type) where + dist : α → α → Nat + +instance : Dist Pt := ⟨fun a b => (a.x - b.x) + (a.y - b.y) + (b.x - a.x) + (b.y - a.y)⟩ + +structure Pt3 extends Pt where + z : Nat + +instance : Dist Pt3 := ⟨fun a b => Dist.dist a.toPt b.toPt + (a.z - b.z) + (b.z - a.z)⟩ + +def d3 (a b : Pt3) : Nat := Dist.dist a b + +class Sz (α : Type) (β : outParam Type) where + sz : α → β + +instance : Sz (List α) Nat := ⟨List.length⟩ + +example (l : List Nat) : Nat := Sz.sz l + d3 ⟨⟨1, 2⟩, 3⟩ ⟨⟨4, 5⟩, 6⟩ + +-- Matcher creation and equation realization inside proofs. +def classify : List Nat → Nat + | [] => 0 + | [x] => x + | _ :: _ :: _ => 2 + +example : classify [] = 0 := by simp [classify] +example : classify [7] = 7 := by simp [classify] +example (x y : Nat) (l : List Nat) : classify (x :: y :: l) = 2 := by simp [classify] + +-- Structural recursion (def height overrides) and generated equations. +def sumUp : Nat → Nat + | 0 => 0 + | n + 1 => n + 1 + sumUp n + +example : sumUp 3 = 6 := by simp [sumUp] + +-- Reducibility: a definition guarding an instance, then a post-hoc change observed by a query. +def Wrapped := Nat + +example : (inferInstance : Dist Pt).dist ⟨0, 0⟩ ⟨1, 1⟩ = 2 := rfl + +attribute [reducible] Wrapped + +instance : Dist Wrapped := ⟨fun a b => (a : Nat) + (b : Nat)⟩ + +example : Dist.dist (2 : Wrapped) (3 : Wrapped) = 5 := rfl + +-- Auxiliary recursors and noConfusion on an inductive family. +inductive Tree (α : Type) where + | leaf : Tree α + | node : Tree α → α → Tree α → Tree α + +def Tree.size : Tree α → Nat + | .leaf => 0 + | .node l _ r => l.size + 1 + r.size + +instance : Dist (Tree Nat) := ⟨fun a b => a.size + b.size⟩ + +example (t : Tree Nat) : Dist.dist t t = 2 * t.size := by + simp [Dist.dist, Nat.two_mul] diff --git a/tests/elab/tc_cache_reducibility_birth.lean b/tests/elab/tc_cache_reducibility_birth.lean new file mode 100644 index 000000000000..b636f218a8e8 --- /dev/null +++ b/tests/elab/tc_cache_reducibility_birth.lean @@ -0,0 +1,45 @@ +import Lean.Elab.Command + +/-! +Tests that reducibility changes invalidate the type class resolution cache within a command by +birth arithmetic: a change whose target was born after a cached entry's query is skipped during +validation (the query cannot have observed it), while a change to a pre-existing declaration +invalidates the entry. See `Lean.Environment.declChangeLog`. +-/ + +open Lean Meta Elab Command + +class R (α : Type) where + +instance : R Nat := ⟨⟩ + +def MyNat := Nat + +-- `MyNat` is semireducible, so resolution cannot unfold it and the failure is cached (`new:` +-- then `cached:`). Marking a *freshly created* constant `[reducible]` leaves the entry alive: +-- the constant was born after the entry's watermark, so the change is skipped (`cached:`). +-- Marking pre-existing `MyNat` `[reducible]` invalidates the entry; `MyNat` now unfolds and the +-- query succeeds (`new:` then `cached:`). +/-- +trace: [Meta.synthInstance.cache] new: R MyNat +[Meta.synthInstance.cache] cached: R MyNat +[Meta.synthInstance.cache] cached: R MyNat +[Meta.synthInstance.cache] new: R MyNat +[Meta.synthInstance.cache] cached: R MyNat +-/ +#guard_msgs in +run_cmd liftTermElabM do + let ty := mkApp (mkConst ``R) (mkConst ``MyNat) + let query : TermElabM Unit := + withOptions (·.setBool `trace.Meta.synthInstance.cache true) do + discard <| synthInstance? ty + query + query + addDecl <| .defnDecl { + name := `freshHelper, levelParams := [], type := mkConst ``Nat, + value := mkNatLit 1, hints := .abbrev, safety := .safe } + Attribute.add `freshHelper `reducible .missing + query + Attribute.add ``MyNat `reducible .missing + query + query From b2a585fcf3f2f5f36193449a7ea42a3b07ff800a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 31 Jul 2026 19:18:02 +0000 Subject: [PATCH 3/3] feat: persist context-free type class resolution cache entries across commands Cache entries whose key contains no metavariables and whose value is closed (no free variables or abstracted metavariables in key or value) are additionally stored in a persistent tier that survives the current command, so identical queries in later commands are served from the cache instead of re-searched. The recorded dependencies introduced in the previous PR replace whole-cache invalidation entirely: an entry from an earlier command is only served while its recorded option lookups, extension generations, and reducibility statuses still give the same answers, so instance declarations, unification hints, and reducibility changes invalidate exactly the affected entries. The persistent tier lives in a dedicated `Environment` field with branch-local value semantics: fills roll back with the environment (e.g. when a speculatively added instance is discarded), parallel elaboration branches never observe each other's fills, and a fill costs one structure copy. Context-sensitive results (metavariable-laden keys, free-variable-dependent entries) stay in the per-command tier; in particular, free-variable-keyed entries must not be persisted, as `FVarId`s recur across commands under fresh name generators (see the `tc_cache_persist_fvar` test). The behavioral test suite for dependency recording arrives here, as most of it is only observable across commands: decl-time vs post-hoc reducibility changes, option partitioning with coexisting entries, fine-grained unification-hint invalidation, and erased-instance scoping. Co-Authored-By: Claude Fable 5 --- src/Lean/Environment.lean | 13 ++ src/Lean/Meta/Instances.lean | 54 ++++- src/Lean/Meta/SynthInstance.lean | 53 ++++- tests/elab/tc_cache_invalidation.lean | 141 +++++++++++++ tests/elab/tc_cache_options_key.lean | 52 +++++ tests/elab/tc_cache_persist.lean | 185 ++++++++++++++++++ tests/elab/tc_cache_persist_fvar.lean | 44 +++++ tests/elab/tc_cache_persist_transparency.lean | 40 ++++ tests/elab_fail/eraseInsts.lean | 10 + tests/elab_fail/eraseInsts.lean.out.expected | 4 + 10 files changed, 581 insertions(+), 15 deletions(-) create mode 100644 tests/elab/tc_cache_invalidation.lean create mode 100644 tests/elab/tc_cache_options_key.lean create mode 100644 tests/elab/tc_cache_persist.lean create mode 100644 tests/elab/tc_cache_persist_fvar.lean create mode 100644 tests/elab/tc_cache_persist_transparency.lean diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 782886499983..bd25222439d1 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -681,6 +681,15 @@ structure Environment where -/ recordArmBirthGen : Nat := 0 /-- + Persistent tier of the type class resolution cache, `none` for empty. The value is a + `Lean.Meta.SynthInstanceCache` (not nameable in this module; accessed with confined casts in + `Lean.Meta.Instances`). It lives in a plain field rather than an environment extension so that + a cache fill costs one structure copy instead of copying the extension state array, while + keeping the same branch-local value semantics: fills roll back with the environment, and + parallel elaboration branches never observe each other's fills. + -/ + synthCacheRaw? : Option NonScalar := none + /-- Counter bumped by every modification a recorded dependency could refer to: any state change of a generation-tracked extension and every post-hoc reducibility change. Cache entries are stamped with it (`RecordedDeps.recordGen`); while it is unchanged, validation skips @@ -781,6 +790,10 @@ def checkDeclChangeLog (env : Environment) (fromPos birthW : Nat) : Bool := fromPos ≤ env.declChangeLog.size && env.declChangeLog.all (fun d => env.constBirthIdx d > birthW) (start := fromPos) +/-- Updates `env.synthCacheRaw?`; see there. -/ +def setSynthCacheRaw? (env : Environment) (v? : Option NonScalar) : Environment := + { env with synthCacheRaw? := v? } + /-- Updates `env.isRecordingDeps`; arming also stamps `Environment.recordArmBirthGen`. -/ def setRecordingDeps (env : Environment) (recording : Bool) : Environment := if recording then diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 8423864cdead..dea8b0a16a17 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -118,17 +118,61 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In trackGen := true } +private unsafe def getSynthCacheUnsafe (env : Environment) : SynthInstanceCache := + match env.synthCacheRaw? with + | some v => unsafeCast v + | none => {} + +/-- +Persistent tier of the `synthInstance` result cache, stored in `Environment.synthCacheRaw?`; +see there and `Lean.Meta.SynthInstance`. It persists across commands and is not stored in +`.olean` files. + +Only *context-free* entries are stored here: keys without metavariables and closed results. +Context-sensitive entries (whose validity depends on the ambient metavariable context) live in +the transient `Meta.Cache.synthInstance` tier instead. + +Both fills and invalidation are plain (branch-local) environment modifications: an entry is +only ever observable in environments derived from the one it was filled in, so rolling back the +environment (e.g. discarding a speculatively added instance) also rolls back the entries that +were computed with it, and parallel elaboration branches never observe each other's fills. +Entries persisted within a rolled-back region are lost with it; within a single command the +transient tier compensates, as `Meta.Cache` is deliberately not restored by +`Meta.SavedState.restore` (see `Lean.Meta.SynthInstance.insertCachedResult`). +-/ +@[implemented_by getSynthCacheUnsafe] +opaque _root_.Lean.Environment.synthCache (env : Environment) : SynthInstanceCache + +private unsafe def setSynthCacheUnsafe (env : Environment) (c : SynthInstanceCache) : Environment := + env.setSynthCacheRaw? (some (unsafeCast c)) + +/-- Replaces the persistent tier of the `synthInstance` result cache; see `Environment.synthCache`. -/ +@[implemented_by setSynthCacheUnsafe] +opaque _root_.Lean.Environment.setSynthCache (env : Environment) (c : SynthInstanceCache) : Environment + +/-- +Resets the persistent tier of the type class resolution cache. Use `resetSynthInstanceCache` +instead from `MetaM`, which also clears the transient `Meta.Cache.synthInstance` tier; +context-free entries are written to both tiers (see `Lean.Meta.SynthInstance.insertCachedResult`). +-/ +def resetSynthInstanceCacheCore : CoreM Unit := + modify fun s => { s with env := s.env.setSynthCacheRaw? none } + /-- -Resets the type class resolution cache (`Meta.Cache.synthInstance`). +Resets the type class resolution cache (both the persistent tier and the transient +`Meta.Cache.synthInstance` tier). Calling this function is normally unnecessary: cache entries record the dependencies of their search (relevant options, instances, unification hints, reducibility statuses; see -`Lean.Meta.SynthInstance`) and are automatically invalidated when a dependency changes. Known -remaining gaps that do require an explicit reset: deactivation of *scoped* unification hints -(ending the surrounding scope or section), and dropping *local* unification hints at the end of -a section, neither of which is covered by the cache key or the recorded dependencies. +`Lean.Meta.SynthInstance`) and are automatically invalidated when a dependency changes, +including through environment modifications the current `Meta.State` cannot observe (e.g. +running a command via `liftCommandElabM`). Known remaining gaps that do require an explicit +reset: deactivation of *scoped* unification hints (ending the surrounding scope or section), +and dropping *local* unification hints at the end of a section, neither of which is covered by +the cache key or the recorded dependencies. -/ def resetSynthInstanceCache : MetaM Unit := do + resetSynthInstanceCacheCore modifyCache fun c => { c with synthInstance := {} } private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 23c6204a2747..a19a8625b7cf 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -957,16 +957,32 @@ private def sameDepIdentity (a b : RecordedDeps) : Bool := && a.extGens.all (fun d => b.extGens.any (·.1 == d.1)) /-- -Inserts a result into the type class resolution cache (`Meta.Cache.synthInstance`), which has -the lifetime of the current `Meta.State`; note that `Meta.SavedState.restore` deliberately does -not restore `Meta.Cache`, so entries survive backtracking (e.g. tactics trying alternatives) -within a command. +Inserts a result into the type class resolution cache: always into the transient +`Meta.Cache.synthInstance` tier, which has the lifetime of the current `Meta.State`, and +additionally into the persistent tier if `persist` is true. + +Only context-free entries may be persisted: the key must not contain metavariables and the result +must be closed. Results with abstracted metavariables are only valid relative to the elaboration +context that created them: their degrees of freedom (e.g. universe metavariables not determined +by the key, cf. `Small`) are resolved by ambient constraints, so reusing them in a different +context can produce incorrectly instantiated terms. + +A persistent insertion is rolled back together with the environment (see +`Environment.synthCache`); the transient copy then still serves the entry for the rest of the +command, as `Meta.SavedState.restore` deliberately does not restore `Meta.Cache`. Without it, +backtracking-heavy elaboration (e.g. tactics trying alternatives) would re-run every failed +attempt's typeclass queries from scratch. -/ private def insertCachedResult (key : SynthInstanceCacheKey) (log : RecordedDeps) - (result? : Option AbstractMVarsResult) : MetaM Unit := do + (result? : Option AbstractMVarsResult) (persist : Bool) : MetaM Unit := do -- One entry per observed dependency combination; replace an entry with the same identity. let upsert (c : SynthInstanceCache) : SynthInstanceCache := c.insert key <| (log, result?) :: (c.find? key |>.getD [] |>.filter fun e => !sameDepIdentity e.1 log) + if persist then + -- Modify the environment directly instead of via `Meta.modifyEnv`, which would reset the + -- `Meta.Cache` caches. + modifyThe Core.State fun s => + { s with env := s.env.setSynthCache (upsert s.env.synthCache) } modifyCache fun c => { c with synthInstance := upsert c.synthInstance } /-- @@ -997,9 +1013,10 @@ private def validateDeps? (opts : Options) (env : Environment) /-- Returns the type class resolution cache entry for `key` from the transient -(`Meta.Cache.synthInstance`), together with its recorded dependencies. Only entries whose -recorded dependencies give the same answers in the current context are considered -(`validateDeps?`); a re-stamped entry is re-inserted. See `SynthInstanceCache`. +(`Meta.Cache.synthInstance`) or persistent (`Environment.synthCache`) tier, together with its +recorded dependencies. Only entries whose recorded dependencies give the same answers in the +current context are considered (`validateDeps?`); a re-stamped entry is re-inserted into its +tier. See `SynthInstanceCache`. -/ private def findCachedResult? (key : SynthInstanceCacheKey) : MetaM (Option (RecordedDeps × Option AbstractMVarsResult)) := do @@ -1015,7 +1032,11 @@ private def findCachedResult? (key : SynthInstanceCacheKey) : return none if let some (log, val?, restamped) ← findIn (← get).cache.synthInstance then if restamped then - insertCachedResult key log val? + insertCachedResult key log val? (persist := false) + return some (log, val?) + if let some (log, val?, restamped) ← findIn env.synthCache then + if restamped then + insertCachedResult key log val? (persist := true) return some (log, val?) return none @@ -1049,7 +1070,19 @@ private def cacheResult (cacheKey : SynthInstanceCacheKey) (log : RecordedDeps) result?.map fun result => { expr := result, paramNames := #[], mvars := #[] } else some abstResult - insertCachedResult cacheKey log value? + -- Only context-free entries may be persisted: a mvar-free key (`.noMVars`), no free variable in + -- the key or the value, and a closed value (no abstracted metavariables); see + -- `insertCachedResult`. + -- + -- A free variable identifies a variable only within the `NameGenerator` that created it, and the + -- cache outlives any of them: the pretty printer and the info tree each run with a fresh + -- generator (`PPContext.runCoreM`), so a delaborator that synthesizes an instance produces the + -- very same `FVarId`s in every command. An entry keyed by one would then be served to an + -- unrelated query over an identically named but differently typed variable. + let persist := kind matches .noMVars && + cacheKey.localInsts.isEmpty && !cacheKey.type.hasFVar && + (value?.all fun r => r.numMVars == 0 && r.paramNames.isEmpty && !r.expr.hasFVar) + insertCachedResult cacheKey log value? (persist := persist) /-- The `Meta.Config` used for all type class resolution. The ambient configuration is replaced diff --git a/tests/elab/tc_cache_invalidation.lean b/tests/elab/tc_cache_invalidation.lean new file mode 100644 index 000000000000..9390730c290c --- /dev/null +++ b/tests/elab/tc_cache_invalidation.lean @@ -0,0 +1,141 @@ +/-! +Tests that the persistent type class resolution cache is invalidated by post-hoc environment +changes that affect definitional equality during resolution: reducibility attribute changes and +new unification hints. A reducibility attribute applied as part of a declaration's own +elaboration does not invalidate the cache, since no cached entry can mention the new declaration. +-/ + +set_option trace.Meta.synthInstance.cache true + +class R (α : Type) where + +instance : R Nat := ⟨⟩ + +def MyNat := Nat + +-- `MyNat` is semireducible, so resolution cannot unfold it: the failure is cached. +/-- +error: failed to synthesize instance of type class + R MyNat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: R MyNat +-/ +#guard_msgs in +def r1 : Unit := let _ : R MyNat := inferInstance; () + +/-- +error: failed to synthesize instance of type class + R MyNat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] cached: R MyNat +-/ +#guard_msgs in +def r2 : Unit := let _ : R MyNat := inferInstance; () + +-- A reducibility attribute that is part of a declaration's own elaboration does not reset the +-- cache: the entry above is still served. +@[reducible] def OtherNat := Nat + +/-- +error: failed to synthesize instance of type class + R MyNat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] cached: R MyNat +-/ +#guard_msgs in +def r3 : Unit := let _ : R MyNat := inferInstance; () + +-- A post-hoc reducibility change resets the cache; `MyNat` now unfolds during resolution and the +-- query succeeds. +attribute [reducible] MyNat + +/-- trace: [Meta.synthInstance.cache] new: R MyNat -/ +#guard_msgs in +def r4 : Unit := let _ : R MyNat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: R MyNat -/ +#guard_msgs in +def r5 : Unit := let _ : R MyNat := inferInstance; () + +-- All declarations happen up front so that no instance addition (which invalidates every entry +-- that consulted the instance table) interferes with the queries below. +class OP (α : Type) (β : outParam Type) where + +instance : OP Nat Bool := ⟨⟩ + +def NotBool := List Nat + +def YetAnotherNat := Nat + +-- The `R Nat` search succeeds without any failing unification, so it never consults the +-- unification hints and records no dependency on them: adding a hint below must not invalidate +-- this entry. +/-- trace: [Meta.synthInstance.cache] new: R Nat -/ +#guard_msgs in +def q1 : Unit := let _ : R Nat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: R Nat -/ +#guard_msgs in +def q2 : Unit := let _ : R Nat := inferInstance; () + +-- A query whose output parameter fails to unify does consult the hints on the failure path and +-- records the dependency; the failure is cached with it. +/-- +error: failed to synthesize instance of type class + OP Nat NotBool + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: OP Nat NotBool +-/ +#guard_msgs in +def q3 : Unit := let _ : OP Nat NotBool := inferInstance; () + +/-- +error: failed to synthesize instance of type class + OP Nat NotBool + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] cached: OP Nat NotBool +-/ +#guard_msgs in +def q4 : Unit := let _ : OP Nat NotBool := inferInstance; () + +-- The hint is irrelevant to both cached queries, but only the `OP` search consulted the hint +-- table: adding the hint invalidates exactly that entry. +@[unification_hint] def yetAnotherHint : Prop := YetAnotherNat = Nat + +/-- +error: failed to synthesize instance of type class + OP Nat NotBool + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: OP Nat NotBool +-/ +#guard_msgs in +def q5 : Unit := let _ : OP Nat NotBool := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: R Nat -/ +#guard_msgs in +def q6 : Unit := let _ : R Nat := inferInstance; () + +-- A post-hoc reducibility change (here: overriding an imported declaration) bumps the change +-- counter and conservatively invalidates every earlier entry, including entries whose search +-- never consulted the declaration. +attribute [local implicit_reducible] Function.const + +/-- trace: [Meta.synthInstance.cache] new: R Nat -/ +#guard_msgs in +def q7 : Unit := let _ : R Nat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: R Nat -/ +#guard_msgs in +def q8 : Unit := let _ : R Nat := inferInstance; () diff --git a/tests/elab/tc_cache_options_key.lean b/tests/elab/tc_cache_options_key.lean new file mode 100644 index 000000000000..f2dcb1144c99 --- /dev/null +++ b/tests/elab/tc_cache_options_key.lean @@ -0,0 +1,52 @@ +/-! +Tests that the type class resolution cache tracks options by *recorded accesses*: every +result-relevant option lookup on the search path is recorded as a dependency of the cache entry +(`Lean.getRecordedOption`), and an entry is reused exactly when its recorded lookups give the +same answers. Options the search never read do not partition the cache, result-irrelevant +options (e.g. pretty printing) are never recorded, and plainly acquiring the options on the +search path panics (`Core.Context.recordingDeps`), so no access can go untracked; the frameworks +whose reads cannot influence results (trace collection, limits) acquire them via +`getOptionsUnrestricted` at their accessors. +-/ + +set_option trace.Meta.synthInstance.cache true + +class Boo (α : Type) where + +instance : Boo Nat := ⟨⟩ + +/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/ +#guard_msgs in +def b1 : Unit := let _ : Boo Nat := inferInstance; () + +-- Result-irrelevant options do not partition the cache. +set_option pp.universes true in +/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/ +#guard_msgs in +def b2 : Unit := let _ : Boo Nat := inferInstance; () + +-- A result-relevant option the search never read does not partition the cache either: this +-- search never invokes `synthPending`, so `maxSynthPendingDepth` is not among its recorded +-- dependencies. +set_option maxSynthPendingDepth 2 in +/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/ +#guard_msgs in +def b3 : Unit := let _ : Boo Nat := inferInstance; () + +-- An option the search did read invalidates: every search consults +-- `backward.synthInstance.canonInstances`, so changing it forces a fresh entry. +set_option backward.synthInstance.canonInstances false in +/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/ +#guard_msgs in +def b4 : Unit := let _ : Boo Nat := inferInstance; () + +-- Entries for both observed values coexist: back at the default, `b1`'s entry is reused … +/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/ +#guard_msgs in +def b5 : Unit := let _ : Boo Nat := inferInstance; () + +-- … and the entry recorded under the changed value remains valid in its setting. +set_option backward.synthInstance.canonInstances false in +/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/ +#guard_msgs in +def b6 : Unit := let _ : Boo Nat := inferInstance; () diff --git a/tests/elab/tc_cache_persist.lean b/tests/elab/tc_cache_persist.lean new file mode 100644 index 000000000000..10dfd2b365c7 --- /dev/null +++ b/tests/elab/tc_cache_persist.lean @@ -0,0 +1,185 @@ +/-! +Tests that the type class resolution cache persists across commands, is reset when instances are +added or erased, and keys entries by the set of activated scoped instances and of local +instances. + +Persistent cache fills are environment modifications, so they are rolled back together with the +environment; in particular `example`s (which are elaborated inside `withoutModifyingEnv`) can +read the cache but do not contribute new entries to it. +-/ + +set_option trace.Meta.synthInstance.cache true + +class Boo (α : Type) where + +instance booNat : Boo Nat := ⟨⟩ + +/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/ +#guard_msgs in +def b1 : Unit := let _ : Boo Nat := inferInstance; () + +-- The result is cached across commands. +/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/ +#guard_msgs in +def b2 : Unit := let _ : Boo Nat := inferInstance; () + +class Coo (α : Type) where + +-- Failures are cached as well, including across commands. +/-- +error: failed to synthesize instance of type class + Coo Nat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: Coo Nat +-/ +#guard_msgs in +def c1 : Unit := let _ : Coo Nat := inferInstance; () + +/-- +error: failed to synthesize instance of type class + Coo Nat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] cached: Coo Nat +-/ +#guard_msgs in +def c2 : Unit := let _ : Coo Nat := inferInstance; () + +-- Adding an instance resets the cache, so the cached failure above is discarded. +instance : Coo Nat := ⟨⟩ + +/-- trace: [Meta.synthInstance.cache] new: Coo Nat -/ +#guard_msgs in +def c3 : Unit := let _ : Coo Nat := inferInstance; () + +-- The reset clears the whole cache, including unrelated entries. +/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/ +#guard_msgs in +def b3 : Unit := let _ : Boo Nat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/ +#guard_msgs in +def b4 : Unit := let _ : Boo Nat := inferInstance; () + +-- Erasing an instance resets the cache. +attribute [-instance] booNat + +/-- +error: failed to synthesize instance of type class + Boo Nat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: Boo Nat +-/ +#guard_msgs in +def b5 : Unit := let _ : Boo Nat := inferInstance; () + +class Doo (α : Type) where + +namespace N +scoped instance dooNat : Doo Nat := ⟨⟩ +end N + +/-- +error: failed to synthesize instance of type class + Doo Nat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: Doo Nat +-/ +#guard_msgs in +def d1 : Unit := let _ : Doo Nat := inferInstance; () + +-- Activating a scoped instance via `open` switches to a different cache key partition, so the +-- cached failure above is not consulted and synthesis succeeds. +open N in +/-- trace: [Meta.synthInstance.cache] new: Doo Nat -/ +#guard_msgs in +def d2 : Unit := let _ : Doo Nat := inferInstance; () + +-- After the scope ends, the entries from before the `open` are valid again. +/-- +error: failed to synthesize instance of type class + Doo Nat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] cached: Doo Nat +-/ +#guard_msgs in +def d3 : Unit := let _ : Doo Nat := inferInstance; () + +-- Re-activating the scope makes the entries cached inside the previous `open` valid again. +open N + +/-- trace: [Meta.synthInstance.cache] cached: Doo Nat -/ +#guard_msgs in +def d4 : Unit := let _ : Doo Nat := inferInstance; () + +-- Local instances are part of the cache key as well, so entries computed with a local instance +-- do not leak out of its scope. +class Eoo (α : Type) where + +@[instance_reducible] def eooNat : Eoo Nat := ⟨⟩ + +section +attribute [local instance] eooNat + +/-- trace: [Meta.synthInstance.cache] new: Eoo Nat -/ +#guard_msgs in +def e1 : Unit := let _ : Eoo Nat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: Eoo Nat -/ +#guard_msgs in +def e2 : Unit := let _ : Eoo Nat := inferInstance; () + +end + +/-- +error: failed to synthesize instance of type class + Eoo Nat + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +trace: [Meta.synthInstance.cache] new: Eoo Nat +-/ +#guard_msgs in +def e3 : Unit := let _ : Eoo Nat := inferInstance; () + +-- `example`s do not contribute cache entries: their environment changes, including cache fills, +-- are reverted. +class Foo (α : Type) where + +instance : Foo Nat := ⟨⟩ + +/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/ +#guard_msgs in +example : Foo Nat := inferInstance + +/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/ +#guard_msgs in +def f1 : Unit := let _ : Foo Nat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: Foo Nat -/ +#guard_msgs in +def f2 : Unit := let _ : Foo Nat := inferInstance; () + +-- `synthInstance.maxSize` is part of the cache key, so cached results (in particular failures) +-- obtained under a different size limit are not reused. +/-- trace: [Meta.synthInstance.cache] new: Coo Nat -/ +#guard_msgs in +def c4 : Unit := let _ : Coo Nat := inferInstance; () + +/-- trace: [Meta.synthInstance.cache] cached: Coo Nat -/ +#guard_msgs in +def c5 : Unit := let _ : Coo Nat := inferInstance; () + +set_option synthInstance.maxSize 100 in +/-- trace: [Meta.synthInstance.cache] new: Coo Nat -/ +#guard_msgs in +def c6 : Unit := let _ : Coo Nat := inferInstance; () diff --git a/tests/elab/tc_cache_persist_fvar.lean b/tests/elab/tc_cache_persist_fvar.lean new file mode 100644 index 000000000000..933e9a068925 --- /dev/null +++ b/tests/elab/tc_cache_persist_fvar.lean @@ -0,0 +1,44 @@ +import Lean + +/-! +Tests that free-variable-dependent type class resolution cache entries are not persisted across +commands. + +A `FVarId` identifies a variable only within the `NameGenerator` that created it. The pretty +printer runs with a fresh one (`PPContext.runCoreM`), so a delaborator that synthesizes an instance +under a binder sees the same `FVarId`s in every command. Persisting an entry keyed by such a +variable makes the next command's unrelated query hit it. Reduced from Mathlib's `max`/`⊔` +delaborator, which decides on notation by testing for a `LinearOrder` instance. +-/ + +open Lean + +class Foo (α : Type) where +class Bar (α : Type) where + +def wrap {α : Type} (a : α) : α := a + +open Lean Meta PrettyPrinter Delaborator SubExpr in +@[delab app.wrap] +def delabWrap : Delab := do + let e ← getExpr + guard (e.getAppNumArgs == 2) + let α := e.appFn!.appArg! + -- The pretty printer clears the local instances, so re-add them, as Mathlib's delaborator does. + let decls := (← getLCtx).decls.toList.filterMap id + let r? ← withLocalInstances decls do + synthInstance? (mkApp (mkConst ``Foo) α) + let a ← withAppArg delab + let tag := mkIdent (if r?.isSome then `FOO else `NOFOO) + `($tag $a) + +-- Delaborating this fails to synthesize `Foo _pp_uniq.1`. +/-- info: fun α [Bar α] a => NOFOO a : (α : Type) → [Bar α] → α → α -/ +#guard_msgs in +#check fun (α : Type) [Bar α] (a : α) => wrap a + +-- The binder is a different variable that merely reuses the `FVarId`, and `Foo` is synthesizable +-- from it, so the failure above must not be reused. +/-- info: fun α [Foo α] a => FOO a : (α : Type) → [Foo α] → α → α -/ +#guard_msgs in +#check fun (α : Type) [Foo α] (a : α) => wrap a diff --git a/tests/elab/tc_cache_persist_transparency.lean b/tests/elab/tc_cache_persist_transparency.lean new file mode 100644 index 000000000000..97ea5ed4cf91 --- /dev/null +++ b/tests/elab/tc_cache_persist_transparency.lean @@ -0,0 +1,40 @@ +/-! +Tests option-dependency recording on the `backward.isDefEq.respectTransparency` options, which +decide whether `isDefEq` bumps the transparency when assigning a metavariable. They belong to the +per-query resolved flags (`Lean.Meta.SynthDefEqFlags`): every query records them up front, so +toggling them partitions the cache regardless of whether the search reached the corresponding +reads. See `tc_cache_options_key.lean` for a lazily recorded option that only partitions the +queries that read it. +-/ + +set_option trace.Meta.synthInstance.cache true + +class Foo (α : Type) where + +instance fooNat : Foo Nat := ⟨⟩ + +/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/ +#guard_msgs in +def a1 : Unit := let _ : Foo Nat := inferInstance; () + +-- A different `backward.isDefEq.respectTransparency` partitions the cache. +set_option backward.isDefEq.respectTransparency false in +/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/ +#guard_msgs in +def a2 : Unit := let _ : Foo Nat := inferInstance; () + +-- Likewise for `backward.isDefEq.respectTransparency.types`. +set_option backward.isDefEq.respectTransparency.types false in +/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/ +#guard_msgs in +def a3 : Unit := let _ : Foo Nat := inferInstance; () + +-- The entries of all partitions remain valid. +/-- trace: [Meta.synthInstance.cache] cached: Foo Nat -/ +#guard_msgs in +def a4 : Unit := let _ : Foo Nat := inferInstance; () + +set_option backward.isDefEq.respectTransparency false in +/-- trace: [Meta.synthInstance.cache] cached: Foo Nat -/ +#guard_msgs in +def a5 : Unit := let _ : Foo Nat := inferInstance; () diff --git a/tests/elab_fail/eraseInsts.lean b/tests/elab_fail/eraseInsts.lean index f53ecb9c413c..e04811694d90 100644 --- a/tests/elab_fail/eraseInsts.lean +++ b/tests/elab_fail/eraseInsts.lean @@ -13,3 +13,13 @@ def f2 (a b : Foo) := a + b -- Error end def f3 (a b : Foo) := a + b + +-- Same, with an explicit result type so that the failed query is metavariable-free and its +-- cached failure reaches the persistent (cross-command) cache tier. +section +attribute [-instance] fooAdd + +def g2 (a b : Foo) : Foo := a + b -- Error +end + +def g3 (a b : Foo) : Foo := a + b diff --git a/tests/elab_fail/eraseInsts.lean.out.expected b/tests/elab_fail/eraseInsts.lean.out.expected index 7c9b54ffd094..6f424e83fe9b 100644 --- a/tests/elab_fail/eraseInsts.lean.out.expected +++ b/tests/elab_fail/eraseInsts.lean.out.expected @@ -2,3 +2,7 @@ eraseInsts.lean:12:22-12:27: error(lean.synthInstanceFailed): failed to synthesi HAdd Foo Foo ?m Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +eraseInsts.lean:22:28-22:33: error(lean.synthInstanceFailed): failed to synthesize instance of type class + HAdd Foo Foo ?m + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.