chore: bump toolchain to v4.29.0-rc7

Aesop/ElabM.lean

@@ -47,7 +47,7 @@ abbrev ElabM := ReaderT ElabM.Context $ TermElabM
 -- Generate specialized pure/bind implementations so we don't need to optimise
 -- them on the fly at each use site.
 instance : Monad ElabM :=
-  { inferInstanceAs (Monad ElabM) with }
+  { (inferInstance : Monad ElabM) with }
 
 protected def ElabM.run (ctx : Context) (x : ElabM α) : TermElabM α := do
   ReaderT.run x ctx

Aesop/Forward/State.lean

@@ -11,7 +11,7 @@ public import Aesop.EMap
 public section
 
 open Lean Lean.Meta
-open ExceptToEmoji (toEmoji)
+
 
 set_option linter.missingDocs true
 
@@ -698,7 +698,7 @@ def eraseHyp (h : FVarId) (pi : PremiseIndex) (rs : RuleState) : RuleState :=
 /-- Add any enqueued hyps to the rule state, potentially generating new
 complete matches in the process. -/
 def update (goal : MVarId) (rs : RuleState) : BaseM (RuleState × Array ForwardRuleMatch) :=
-  withAesopTraceNode .forward (fun r => return m!"{exceptEmoji r} update rule state {rs.rule.name}") do
+  withAesopTraceNode .forward (fun _ => return m!"update rule state {rs.rule.name}") do
   if ! rs.clusterStates.all (·.haveHypForEachSlot) then
     aesop_trace[forward] "skipping update since some cluster states cannot yet have complete matches"
     return (rs, #[])
@@ -895,7 +895,7 @@ def update (goal : MVarId) (fs : ForwardState) (phase? : Option PhaseName) :
     match phase? with
     | none => "all phases"
     | some phase => s!"{phase} phase"
-  withAesopTraceNode .forward (fun r => return m!"{exceptEmoji r} update forward state for {phaseStr}") do
+  withAesopTraceNode .forward (fun _ => return m!"update forward state for {phaseStr}") do
   let toUpdate : Array RuleName :=
     match phase? with
     | none => fs.ruleStates.foldl (init := #[]) fun toUpdate rule _ => toUpdate.push rule

Aesop/Saturate.lean

@@ -68,19 +68,19 @@ where
 
   tryNormRules (goal : MVarId) (mvars : UnorderedArraySet MVarId)
       (preState : Meta.SavedState) : SaturateM (Option GoalDiff) :=
-    withTraceNode `saturate (λ res => return m!"{exceptOptionEmoji res} trying normalisation rules") do
+    withTraceNode `saturate (fun _ => return m!"trying normalisation rules") do
       let matchResults ←
-        withTraceNode `saturate (λ res => return m!"{exceptEmoji res} selecting normalisation rules") do
+        withTraceNode `saturate (fun _ => return m!"selecting normalisation rules") do
         profilingRuleSelection do
         rs.applicableNormalizationRulesWith ∅ goal
           (include? := (isForwardOrDestructRuleName ·.name))
       runFirstRule goal mvars preState matchResults
 
   trySafeRules (goal : MVarId) (mvars : UnorderedArraySet MVarId)
       (preState : Meta.SavedState) : SaturateM (Option GoalDiff) :=
-    withTraceNode `saturate (λ res => return m!"{exceptOptionEmoji res} trying safe rules") do
+    withTraceNode `saturate (fun _ => return m!"trying safe rules") do
       let matchResults ←
-        withTraceNode `saturate (λ res => return m!"{exceptEmoji res} selecting safe rules") do
+        withTraceNode `saturate (fun _ => return m!"selecting safe rules") do
         profilingRuleSelection do
         rs.applicableSafeRulesWith ∅ goal
           (include? := (isForwardOrDestructRuleName ·.name))
@@ -89,7 +89,7 @@ where
   runRule {α} (goal : MVarId) (mvars : UnorderedArraySet MVarId)
       (preState : Meta.SavedState) (matchResult : IndexMatchResult (Rule α)) :
       SaturateM (Option (GoalDiff × Option (Array Script.LazyStep))) := do
-    withTraceNode `saturate (λ res => return m!"{exceptOptionEmoji res} running rule {matchResult.rule.name}") do
+    withTraceNode `saturate (fun _ => return m!"running rule {matchResult.rule.name}") do
     profilingRule matchResult.rule.name (·.isSome) do
     let input := {
       indexMatchLocations := matchResult.locations

Aesop/Script/Step.lean

@@ -127,7 +127,7 @@ def runFirstSuccessfulTacticBuilder (s : LazyStep) : MetaM Tactic :=
 where
   tryTacticBuilder (b : TacticBuilder) : MetaM (Option Tactic) := do
     let tactic ← b
-    withAesopTraceNode .script (λ res => return m!"{exceptOptionEmoji res} {tactic}") do
+    withAesopTraceNode .script (fun _ => return m!"{tactic}") do
       let tacticResult ← observing? do
         runTacticCapturingPostState tactic.uTactic s.preState [s.preGoal]
       let some (actualPostState, actualPostGoals) := tacticResult

Aesop/Script/StructureDynamic.lean

@@ -82,7 +82,7 @@ structure DynStructureResult where
 
 partial def structureDynamicCore (preState : Meta.SavedState) (preGoal : MVarId)
     (uscript : UScript) : MetaM (Option (UScript × Bool)) :=
-  withAesopTraceNode .script (λ r => return m!"{exceptOptionEmoji r} Dynamically structuring the script") do
+  withAesopTraceNode .script (fun _ => return m!"Dynamically structuring the script") do
     aesop_trace[script] "unstructured script:{indentD $ MessageData.joinSep (uscript.map toMessageData |>.toList) "\n"}"
     let (result?, perfect) ← go preState #[preGoal] |>.run uscript
     let some result := result?
@@ -95,15 +95,15 @@ where
     if h : 0 < preGoals.size then
       -- Try to apply the step for the main goal, then solve the remaining goals.
       let firstGoal := preGoals[0]
-      let result? ← withAesopTraceNode .script (λ r => return m!"{exceptOptionEmoji r} Focusing main goal {firstGoal.name}") do
+      let result? ← withAesopTraceNode .script (fun _ => return m!"Focusing main goal {firstGoal.name}") do
         aesop_trace[script] "goal: {firstGoal.name}{← preState.runMetaM' $ addMessageContext $ indentD firstGoal}"
         goStructured preState preGoals preGoals[0]
       match result? with
       | some result => return result
       | none =>
         -- If this fails, apply the chronologically next step and solve the remaining goals.
         modify ({ · with perfect := false })
-        withAesopTraceNode .script (λ r => return m!"{exceptOptionEmoji r} Applying step to chronologically first goal") do
+        withAesopTraceNode .script (fun _ => return m!"Applying step to chronologically first goal") do
           goUnstructured preState preGoals
     else
       return some { script := [], postState := preState }

Aesop/Script/UScriptToSScript.lean

@@ -93,7 +93,7 @@ where
 end StepTree
 
 partial def orderedUScriptToSScript (uscript : UScript) (tacticState : TacticState) : CoreM SScript :=
-  withAesopTraceNode .script (λ e => return m!"{exceptEmoji e} Converting ordered unstructured script to structured script") do
+  withAesopTraceNode .script (fun _ => return m!"Converting ordered unstructured script to structured script") do
   aesop_trace[script] "unstructured script:{indentD $ MessageData.joinSep (uscript.map toMessageData |>.toList) "\n"}"
   let stepTree := uscript.toStepTree
   aesop_trace[script] "step tree:{indentD $ toMessageData stepTree}"

Aesop/Search/SearchM.lean

@@ -53,19 +53,19 @@ namespace SearchM
 -- Generate specialized pure/bind implementations so we don't need to optimise
 -- them on the fly at each use site.
 instance : Monad (SearchM Q) :=
-  { inferInstanceAs (Monad (SearchM Q)) with }
+  { (inferInstance : Monad (SearchM Q)) with }
 
 instance : MonadRef (SearchM Q) :=
-  { inferInstanceAs (MonadRef (SearchM Q)) with }
+  { (inferInstance : MonadRef (SearchM Q)) with }
 
 instance : Inhabited (SearchM Q α) where
   default := failure
 
 instance : MonadState (State Q) (SearchM Q) :=
-  { inferInstanceAs (MonadStateOf (State Q) (SearchM Q)) with }
+  { (inferInstance : MonadStateOf (State Q) (SearchM Q)) with }
 
 instance : MonadReader Context (SearchM Q) :=
-  { inferInstanceAs (MonadReaderOf Context (SearchM Q)) with }
+  { (inferInstance : MonadReaderOf Context (SearchM Q)) with }
 
 instance : MonadLift TreeM (SearchM Q) where
   monadLift x := do

Aesop/Tracing.lean

@@ -146,18 +146,18 @@ variable [Monad m] [MonadTrace m] [MonadLiftT BaseIO m] [MonadLiftT IO m]
     [MonadRef m] [AddMessageContext m] [MonadOptions m] [MonadAlwaysExcept ε m]
 
 @[inline, always_inline]
-def withAesopTraceNode (opt : TraceOption)
+def withAesopTraceNode [ExceptToTraceResult ε α] (opt : TraceOption)
     (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) : m α :=
   withTraceNode opt.traceClass msg k collapsed
 
 @[inline, always_inline]
-def withAesopTraceNodeBefore [ExceptToEmoji ε α] (opt : TraceOption)
+def withAesopTraceNodeBefore [ExceptToTraceResult ε α] (opt : TraceOption)
     (msg : m MessageData) (k : m α) (collapsed := true) : m α :=
   withTraceNodeBefore opt.traceClass (fun _ => msg) k collapsed
 
 @[inline, always_inline]
-def withConstAesopTraceNode (opt : TraceOption) (msg : m MessageData) (k : m α)
-    (collapsed := true) : m α :=
+def withConstAesopTraceNode [ExceptToTraceResult ε α] (opt : TraceOption)
+    (msg : m MessageData) (k : m α) (collapsed := true) : m α :=
   withAesopTraceNode opt (λ _ => msg) k collapsed
 
 end

Aesop/Tree/ExtractScript.lean

@@ -95,7 +95,7 @@ end
 
 @[inline]
 def extractScript : TreeM (UScript × Bool) :=
-  withAesopTraceNode .script (λ r => return m!"{exceptEmoji r} Extract script") do
+  withAesopTraceNode .script (fun _ => return m!"Extract script") do
     (← getRootGoal).extractScriptCore.run
 
 mutual
@@ -131,7 +131,7 @@ mutual
 end
 
 def extractSafePrefixScript : TreeM (UScript × Bool) := do
-  withAesopTraceNode .script (λ r => return m!"{exceptEmoji r} Extract safe prefix script") do
+  withAesopTraceNode .script (fun _ => return m!"Extract safe prefix script") do
     (← getRootGoal).extractSafePrefixScriptCore.run
 
 end Aesop

Aesop/Tree/TreeM.lean

@@ -83,7 +83,7 @@ namespace TreeM
 -- Generate specialized pure/bind implementations so we don't need to optimise
 -- them on the fly at each use site.
 instance : Monad TreeM :=
-  { inferInstanceAs (Monad TreeM) with }
+  { (inferInstance : Monad TreeM) with }
 
 instance (priority := low) : MonadStateOf Tree TreeM where
   get := return (← getThe State).tree

Aesop/Util/EqualUpToIds.lean

@@ -50,7 +50,7 @@ abbrev EqualUpToIdsM :=
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
 @[inline, always_inline]
 instance : Monad EqualUpToIdsM :=
-  { inferInstanceAs (Monad EqualUpToIdsM) with }
+  { (inferInstance : Monad EqualUpToIdsM) with }
 
 protected def EqualUpToIdsM.run' (x : EqualUpToIdsM α)
     (commonMCtx? : Option MetavarContext) (mctx₁ mctx₂ : MetavarContext)

AesopTest/EqualUpToIds.lean

@@ -8,6 +8,8 @@ import Aesop.Util.Basic
 import Aesop.Util.EqualUpToIds
 import Aesop.Tree.RunMetaM
 
+set_option linter.unreachableTactic false
+
 -- Some simple test cases for the EqualUpToIds module. The module is mostly
 -- tested by using it in script validation, which is run on almost all Aesop
 -- calls in the test suite.

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bd58e3506632241b59e406902d5e42b73cdeccce",
+   "rev": "46f6618b9942c1f67ebe3b8051163ddb8d8ff496",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc6",
+   "inputRev": "v4.29.0-rc7",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "aesop",

lakefile.toml

@@ -7,7 +7,7 @@ platformIndependent = true
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "v4.29.0-rc6"
+rev = "v4.29.0-rc7"
 
 [[lean_lib]]
 name = "Aesop"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc6
+leanprover/lean4:v4.29.0-rc7