merge master

Author: kim-em

Aesop/Options/Public.lean

@@ -72,8 +72,9 @@ structure Options where
   /--
   Heartbeat limit for individual Aesop rules. If a rule goes over this limit, it
   fails, but Aesop itself continues until it reaches the limit set by the
-  `maxHeartbeats` option. If `maxRuleHeartbeats = 0`, there is no per-rule
-  limit.
+  `maxHeartbeats` option. If `maxRuleHeartbeats = 0` or `maxRuleHeartbeats` is
+  greater than `maxHeartbeats`, the `maxHeartbeats` limit is used for the
+  individual rules as well.
   -/
   maxRuleHeartbeats := 0
   /--

Aesop/Search/Expansion/Basic.lean

@@ -17,7 +17,7 @@ def runRuleTac (tac : RuleTac) (ruleName : RuleName)
   let result ←
     tryCatchRuntimeEx
       (Sum.inr <$> preState.runMetaM' do
-        withMaxHeartbeats input.options.maxRuleHeartbeats do
+        withAtMostMaxHeartbeats input.options.maxRuleHeartbeats do
           tac input)
       (λ e => return Sum.inl e)
   if ← Check.rules.isEnabled then

Aesop/Util/Basic.lean

@@ -80,8 +80,7 @@ open DiscrTree
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
 
-def getConclusionDiscrTreeKeys (type : Expr) :
-    MetaM (Array Key) :=
+def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
     mkDiscrTreePath conclusion
@@ -416,6 +415,19 @@ def withMaxHeartbeats [Monad m] [MonadLiftT BaseIO m]
   }
   withReader f x
 
+/--
+Runs a computation for at most the given number of heartbeats times 1000 or the
+global heartbeat limit, whichever is lower. Note that heartbeats spent on the
+computation still count towards the global heartbeat count. If 0 is given, the
+global heartbeat limit is used.
+-/
+def withAtMostMaxHeartbeats [Monad m] [MonadLiftT BaseIO m] [MonadLiftT CoreM m]
+    [MonadWithReaderOf Core.Context m] (n : Nat) (x : m α) : m α := do
+  let globalMaxHeartbeats ← getMaxHeartbeats
+  let maxHeartbeats :=
+    if n == 0 then globalMaxHeartbeats else min n globalMaxHeartbeats
+  withMaxHeartbeats maxHeartbeats x
+
 open Lean.Elab Lean.Elab.Term in
 def elabPattern (stx : Syntax) : TermElabM Expr :=
   withRef stx $ withReader adjustCtx $ withSynthesize $ elabTerm stx none

AesopTest/List.lean

@@ -540,7 +540,6 @@ theorem X.append_ne_nil_of_ne_nil_left (s t : List α) : s ≠ [] → s ++ t ≠
 theorem X.append_ne_nil_of_ne_nil_right (s t : List α) : t ≠ [] → s ++ t ≠ [] := by
   induction s <;> aesop
 
-attribute [-simp] append_eq_nil
 @[simp] theorem X.append_eq_nil {p q : List α} : (p ++ q) = [] ↔ p = [] ∧ q = [] := by
   aesop (add 1% cases List)
 
@@ -718,7 +717,7 @@ theorem replicate_right_injective (a : α) : Injective (λ n => replicate n a) :
 /-! ### flatMap -/
 
 instance : Bind List where
-  bind l f := List.flatMap l f
+  bind l f := List.flatMap f l
 
 @[simp] theorem bind_eq_flatMap {α β} (f : α → List β) (l : List α) :
     l >>= f = l.flatMap f := rfl
@@ -892,7 +891,7 @@ theorem last_append (l₁ l₂ : List α) (h : l₂ ≠ []) :
   last (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = last l₂ h := by
   induction l₁ <;> aesop
 
-theorem last_concat {a : α} (l : List α) : last (concat l a) (by exact X.concat_ne_nil a l) = a := by
+theorem last_concat {a : α} (l : List α) : last (concat l a) (X.concat_ne_nil a l) = a := by
   aesop
 
 @[simp] theorem last_singleton (a : α) : last [a] (cons_ne_nil a []) = a := rfl

AesopTest/RulePattern.lean

@@ -23,8 +23,8 @@ example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by
   set_option aesop.check.script false in
   aesop!
   all_goals
-    guard_hyp fwd_2 : 0 ≤ (n : Int)
-    guard_hyp fwd_1 : 0 ≤ (m : Int)
+    guard_hyp fwd : 0 ≤ (n : Int)
+    guard_hyp fwd_2 : 0 ≤ (m : Int)
     falso
 
 @[aesop safe forward (pattern := min x y)]
@@ -44,8 +44,8 @@ axiom triangle (a b : Int) : |a + b| ≤ |a| + |b|
 
 example : |a + b| ≤ |c + d| := by
   aesop!
-  guard_hyp fwd   : |c + d| ≤ |c| + |d|
-  guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
+  guard_hyp fwd_1 : |c + d| ≤ |c| + |d|
+  guard_hyp fwd   : |a + b| ≤ |a| + |b|
   falso
 
 @[aesop safe apply (pattern := (0 : Nat))]

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2e82cd8e5d6462f20ffd810ea0e9460475e0b455",
+   "rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "v4.17.0-rc1",
    "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 = "v4.17.0-rc1"
 
 [[lean_lib]]
 name = "Aesop"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-12-19
+leanprover/lean4:v4.17.0-rc1