Apply global heartbeat limit to individual rules (#192)

leanprover-community · Jan 29, 2025 · b9d5f4f · b9d5f4f
1 parent caa2968
commit b9d5f4f
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 5 deletions.
diff --git a/Aesop/Options/Public.lean b/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
   /--

diff --git a/Aesop/Search/Expansion/Basic.lean b/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

diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
@@ -415,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

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
+   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "v4.16.0-rc2",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "aesop",