fixes for leanprover/lean4#6054

Aesop/RuleTac/ElabRuleTerm.lean

@@ -81,7 +81,7 @@ def elabRuleTermForSimpCore (goal : MVarId) (term : Term) (ctx : Simp.Context)
     elabSimpTheorems (mkSimpArgs term) ctx simprocs isSimpAll
 
 def checkElabRuleTermForSimp (term : Term) (isSimpAll : Bool) : ElabM Unit := do
-  let ctx := { simpTheorems := #[{}] }
+  let ctx ← Simp.mkContext (simpTheorems := #[{}] )
   let simprocs := #[{}]
   discard $ elabRuleTermForSimpCore (← read).goal term ctx simprocs isSimpAll
 

Aesop/Search/Expansion/Simp.lean

@@ -44,7 +44,7 @@ def addLetDeclsToSimpTheorems (ctx : Simp.Context) : MetaM Simp.Context := do
     if ldecl.hasValue && ! ldecl.isImplementationDetail then
       simpTheoremsArray := simpTheoremsArray.modify 0 λ simpTheorems =>
         simpTheorems.addLetDeclToUnfold ldecl.fvarId
-  return { ctx with simpTheorems := simpTheoremsArray }
+  return ctx.setSimpTheorems simpTheoremsArray
 
 def addLetDeclsToSimpTheoremsUnlessZetaDelta (ctx : Simp.Context) :
     MetaM Simp.Context := do
@@ -58,7 +58,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (stats : Simp.Stats := {}) : MetaM SimpResult := do
   let mvarIdOld := mvarId
-  let ctx := { ctx with config.failIfUnchanged := false }
+  let ctx := ctx.setFailIfUnchanged false
   let (result, { usedTheorems := usedSimps, .. }) ←
     Meta.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
       stats
@@ -89,7 +89,7 @@ def simpAll (mvarId : MVarId) (ctx : Simp.Context)
     (simprocs : Simp.SimprocsArray) (stats : Simp.Stats := {}) :
     MetaM SimpResult :=
   mvarId.withContext do
-    let ctx := { ctx with config.failIfUnchanged := false }
+    let ctx := ctx.setFailIfUnchanged false
     let ctx ← addLetDeclsToSimpTheoremsUnlessZetaDelta ctx
     match ← Lean.Meta.simpAll mvarId ctx simprocs stats with
     | (none, stats) => return .solved stats.usedTheorems

Aesop/Search/SearchM.lean

@@ -15,7 +15,8 @@ open Lean.Meta
 
 namespace Aesop
 
-structure NormSimpContext extends Simp.Context where
+structure NormSimpContext where
+  toContext : Simp.Context
   enabled : Bool
   useHyps : Bool
   configStx? : Option Term
@@ -83,10 +84,8 @@ protected def run (ruleSet : LocalRuleSet) (options : Aesop.Options')
     MetaM (α × State Q × Tree × Stats) := do
   let t ← mkInitialTree goal
   let normSimpContext := {
-    config := simpConfig
-    maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth
-    simpTheorems := ruleSet.simpTheoremsArray.map (·.snd)
-    congrTheorems := ← getSimpCongrTheorems
+    toContext := ← Simp.mkContext simpConfig (simpTheorems := ruleSet.simpTheoremsArray.map (·.snd))
+      (congrTheorems := ← getSimpCongrTheorems)
     simprocs := ruleSet.simprocsArray.map (·.snd)
     configStx? := simpConfigStx?
     enabled := options.enableSimp

Aesop/Util/Tactic/Unfold.lean

@@ -14,12 +14,7 @@ namespace Aesop
 -- Lean.Meta.unfoldLocalDecl.
 
 def mkUnfoldSimpContext : MetaM Simp.Context := do
-  return {
-    simpTheorems := #[]
-    congrTheorems := ← getSimpCongrTheorems
-    config := Simp.neutralConfig
-    dischargeDepth := 0
-  }
+  Simp.mkContext Simp.neutralConfig (simpTheorems := #[]) (congrTheorems := ← getSimpCongrTheorems)
 
 @[inline]
 def unfoldManyCore (ctx : Simp.Context) (unfold? : Name → Option (Option Name))

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9ba2e12ce6570b7fed7ad4d3675e5f6632949f2b",
+   "rev": "660dd9dcf375c9ec3820dbf682117f3978c497b4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "lean-pr-testing-6054",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "aesop",

lakefile.toml

@@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "nightly-testing"
+rev = "lean-pr-testing-6054"
 
 [[lean_lib]]
 name = "Aesop"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-12
+leanprover/lean4-pr-releases:pr-release-6054