keep generating unfold theorems on demand for now to avoid stage0 udpate

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 import Lean.Meta.ArgsPacker.Basic
+import Lean.Elab.PreDefinition.WF.Unfold
 import Init.Data.Array.Basic
 
 namespace Lean.Elab.WF
@@ -50,4 +51,19 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
 builtin_initialize
   registerGetEqnsFn getEqnsFor?
 
+
+-- Remove the rest of this file after the next stage update,
+-- as we generate these eagerly now.
+def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
+  let name := Name.str declName unfoldThmSuffix
+  let env ← getEnv
+  if env.contains name then return name
+  let some info := eqnInfoExt.find? env declName | return none
+  mkUnfoldEq info.toEqnInfoCore info.declNameNonRec
+  return some name
+
+builtin_initialize
+  registerGetUnfoldEqnFn getUnfoldFor?
+
+
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -64,7 +64,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
   for preDef in preDefs do
     unless preDef.kind.isTheorem do
       unless (← isProp preDef.type) do
-        WF.mkUnfoldEq preDef preDefNonRec.declName
+        WF.mkUnfoldEq { preDef with } preDefNonRec.declName
   Mutual.addPreDefAttributes preDefs
 
 builtin_initialize registerTraceClass `Elab.definition.wf

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -84,7 +84,8 @@ private partial def mkUnfoldProof (declName declNameNonRec : Name) (type : Expr)
     go mvarId
     instantiateMVars main
 
-def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
+-- TODO: Afer the next stage0 update, change the type to PreDefinition
+def mkUnfoldEq (preDef : EqnInfoCore) (unaryPreDefName : Name) : MetaM Unit := do
   withOptions (tactic.hygienic.set · false) do
     let baseName := preDef.declName
     lambdaTelescope preDef.value fun xs body => do