experiment: persist type class resolution cache across commands

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)

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

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. -/

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,48 @@ 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, 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
+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
 

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]
 

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

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 }
 

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

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}"

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`.

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

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