feat: async linting (#4460)

This PR runs all linters for a single command (together) on a separate
thread from further elaboration, making a first step towards
parallelizing the elaborator.

src/Init/System/IO.lean

@@ -981,3 +981,14 @@ not used concurrently or which are already persistent.
 -/
 @[extern "lean_runtime_mark_persistent"]
 unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a
+
+set_option linter.unusedVariables false in
+/--
+Discards the passed owned reference. This leads to `a` any any object reachable from it never being
+freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
+kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
+would be similarly costly to deallocation). It is still considered a safe operation as it cannot
+lead to undefined behavior.
+-/
+@[extern "lean_runtime_forget"]
+def Runtime.forget (a : α) : BaseIO Unit := return

src/Lean/CoreM.lean

@@ -32,7 +32,7 @@ register_builtin_option maxHeartbeats : Nat := {
 }
 
 register_builtin_option Elab.async : Bool := {
-  defValue := false
+  defValue := true
   descr := "perform elaboration using multiple threads where possible"
 }
 
@@ -356,9 +356,7 @@ Returns the current log and then resets its messages while adjusting `MessageLog
 for incremental reporting during elaboration of a single command.
 -/
 def getAndEmptyMessageLog : CoreM MessageLog :=
-  modifyGet fun s => (s.messages, { s with
-    messages.unreported := {}
-    messages.hadErrors  := s.messages.hasErrors })
+  modifyGet fun s => (s.messages, { s with messages := s.messages.markAllReported })
 
 instance : MonadLog CoreM where
   getRef      := getRef
@@ -417,7 +415,7 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact d
     IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
-      modify ({ · with messages := {}, traceState := { tid } })
+      modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()

src/Lean/Elab/BuiltinCommand.lean

@@ -488,6 +488,9 @@ where
     let mut lines : Array MessageData := #[]
     let decls ← getOptionDecls
     for (name, val) in opts do
+      -- `#guard_msgs` sets this option internally, we don't want it to end up in its output
+      if name == `Elab.async then
+        continue
       let (isSet, isUnknown) :=
         match decls.find? name with
         | some decl => (decl.defValue != val, false)

src/Lean/Elab/Command.lean

@@ -287,7 +287,9 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do
               | Exception.internal _ _ =>
                 logException ex
             finally
-              modify fun s => { savedState with messages := s.messages }
+              -- TODO: it would be good to preserve even more state (#4363) but preserving info
+              -- trees currently breaks from linters adding context-less info nodes
+              modify fun s => { savedState with messages := s.messages, traceState := s.traceState }
 
 /--
 Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
@@ -311,7 +313,7 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
     IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
-      modify ({ · with messages := {}, traceState := { tid } })
+      modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()
@@ -344,6 +346,17 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
 def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit :=
   modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
 
+def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
+  if !Elab.async.get (← getOptions) then
+    withoutModifyingEnv do
+      runLinters stx
+    return
+
+  -- We only start one task for all linters for now as most linters are fast and we simply want
+  -- to unblock elaboration of the next command
+  let lintAct ← wrapAsyncAsSnapshot fun _ => runLinters stx
+  logSnapshotTask { range? := none, task := (← BaseIO.asTask lintAct) }
+
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
 
@@ -547,7 +560,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     -- rather than engineer a general solution.
     unless (stx.find? (·.isOfKind ``Lean.guardMsgsCmd)).isSome do
       withLogging do
-        runLinters stx
+        runLintersAsync stx
   finally
     -- note the order: first process current messages & info trees, then add back old messages & trees,
     -- then convert new traces to messages

src/Lean/Elab/Frontend.lean

@@ -169,6 +169,8 @@ def runFrontend
     IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
 
   let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
+  -- no point in freeing the snapshot graph and all referenced data this close to process exit
+  Runtime.forget snaps
   pure (cmdState.env, !hasErrors)
 
 

src/Lean/Elab/GuardMsgs.lean

@@ -140,8 +140,12 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
         |>.trim |> removeTrailingWhitespaceMarker
     let (whitespace, ordering, specFn) ← parseGuardMsgsSpec spec?
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+    -- disable async elaboration for `cmd` so `msgs` will contain all messages
+    let async := Elab.async.get (← getOptions)
+    modifyScope fun scope => { scope with opts := Elab.async.set scope.opts false }
     -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
     elabCommandTopLevel cmd
+    modifyScope fun scope => { scope with opts := Elab.async.set scope.opts async }
     let msgs := (← get).messages
     let mut toCheck : MessageLog := .empty
     let mut toPassthrough : MessageLog := .empty

src/Lean/Message.lean

@@ -441,6 +441,10 @@ instance : Append MessageLog :=
 def hasErrors (log : MessageLog) : Bool :=
   log.hadErrors || log.unreported.any (·.severity matches .error)
 
+/-- Clears unreported messages while preserving `hasErrors`. -/
+def markAllReported (log : MessageLog) : MessageLog :=
+  { log with unreported := {}, hadErrors  := log.hasErrors }
+
 def errorsToWarnings (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
 

src/runtime/io.cpp

@@ -1460,6 +1460,10 @@ extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /
     return io_result_mk_ok(a);
 }
 
+extern "C" LEAN_EXPORT obj_res lean_runtime_forget(obj_arg /* a */, obj_arg /* w */) {
+    return io_result_mk_ok(box(0));
+}
+
 void initialize_io() {
     g_io_error_nullptr_read = lean_mk_io_user_error(mk_ascii_string_unchecked("null reference read"));
     mark_persistent(g_io_error_nullptr_read);