fix: add missing initHeartbeats

In only one case a `Core.Context` is created from within CoreM, and we inherit from the parent Context the `initHeartbeats`. Otherwise, we get the current heartbeats from IO.

Co-authored-by: Laurent Sartran <[email protected]>

Batteries/Tactic/Lint/Frontend.lean

@@ -100,6 +100,7 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) :
     CoreM (Array (NamedLinter × Std.HashMap Name MessageData)) := do
   let env ← getEnv
   let options ← getOptions -- TODO: sanitize options?
+  let initHeartbeats := (← read).initHeartbeats
 
   let tasks : Array (NamedLinter × Array (Name × Task (Option MessageData))) ←
     linters.mapM fun linter => do
@@ -108,7 +109,7 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) :
         BaseIO.asTask do
           match ← withCurrHeartbeats (linter.test decl)
               |>.run' mkMetaContext
-              |>.run' {options, fileName := "", fileMap := default} {env}
+              |>.run' {options, fileName := "", fileMap := default, initHeartbeats } {env}
               |>.toBaseIO with
           | Except.ok msg? => pure msg?
           | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"

Batteries/Util/Cache.lean

@@ -64,8 +64,9 @@ def Cache.get [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] [MonadLiftT B
       -- TODO: add customization option
       let options := maxHeartbeats.set options <|
         options.get? maxHeartbeats.name |>.getD 1000000
+      let initHeartbeats ← IO.getNumHeartbeats
       let res ← EIO.asTask <|
-        init {} |>.run' {} { options, fileName, fileMap } |>.run' { env }
+        init {} |>.run' {} { options, fileName, fileMap, initHeartbeats } |>.run' { env }
       cache.set (m := BaseIO) (.inr res)
       pure res
   match t.get with