rework

Batteries/Tactic/Lint/Frontend.lean

@@ -95,26 +95,21 @@ producing a list of results.
 -/
 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))) ←
+  let tasks : Array (NamedLinter × Array (Name × Task (Except Exception <| Option MessageData))) ←
     linters.mapM fun linter => do
       let decls ← decls.filterM (shouldBeLinted linter.name)
       (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
-        BaseIO.asTask do
-          match ← withCurrHeartbeats (linter.test decl)
-              |>.run' mkMetaContext -- We use the context used by `Command.liftTermElabM`
-              |>.run' {options, fileName := "", fileMap := default, initHeartbeats} {env}
-              |>.toBaseIO with
-          | Except.ok msg? => pure msg?
-          | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"
+        EIO.asTask <| ← Lean.Core.wrapAsync fun _ => do
+          (linter.test decl) |>.run' mkMetaContext -- We use the context used by `Command.liftTermElabM`
 
   tasks.mapM fun (linter, decls) => do
     let mut msgs : Std.HashMap Name MessageData := {}
-    for (declName, msg?) in decls do
-      if let some msg := msg?.get then
+    for (declName, msgTask) in decls do
+      let msg? ← match msgTask.get with
+      | Except.ok msg? => pure msg?
+      | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"
+
+      if let .some msg := msg? then
         msgs := msgs.insert declName msg
     pure (linter, msgs)
 

Batteries/Util/Cache.lean

@@ -46,27 +46,22 @@ instance : Nonempty (Cache α) := inferInstanceAs <| Nonempty (IO.Ref _)
 /-- Creates a cache with an initialization function. -/
 def Cache.mk (init : MetaM α) : IO (Cache α) := IO.mkRef <| Sum.inl init
 
+@[inherit_doc Core.wrapAsync]
+def _root_.Lean.Meta.wrapAsync (act : Unit → MetaM α) : MetaM (EIO Exception α) := do
+  let metaCtx ← readThe Meta.Context
+  let metaSt ← getThe Meta.State
+  Core.wrapAsync fun _ =>
+    act () |>.run' metaCtx metaSt
+
 /--
 Access the cache. Calling this function for the first time will initialize the cache
 with the function provided in the constructor.
 -/
-def Cache.get [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] [MonadLiftT BaseIO m]
-    [MonadExcept Exception m] (cache : Cache α) : m α := do
+def Cache.get (cache : Cache α) : MetaM α := do
   let t ← match ← ST.Ref.get (m := BaseIO) cache with
     | .inr t => pure t
     | .inl init =>
-      let env ← getEnv
-      let fileName ← getFileName
-      let fileMap ← getFileMap
-      let options ← getOptions -- TODO: sanitize options?
-      -- Default heartbeats to a reasonable value.
-      -- otherwise exact? times out on mathlib
-      -- 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, initHeartbeats } |>.run' { env }
+      let res ← EIO.asTask <| ← Meta.wrapAsync fun _ => init
       cache.set (m := BaseIO) (.inr res)
       pure res
   match t.get with