feat: asynchronous kernel checking

src/Lean/AddDecl.lean

@@ -59,18 +59,49 @@ where go env
   | _        => env
 
 def addDecl (decl : Declaration) : CoreM Unit := do
+  let mut env ← getEnv
+  -- register namespaces for newly added constants; this used to be done by the kernel itself
+  -- but that is incompatible with moving it to a separate task
+  env := decl.getNames.foldl registerNamePrefixes env
+  if let .inductDecl _ _ types _ := decl then
+    env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
+
+  if !Elab.async.get (← getOptions) then
+    return (← doAdd)
+
+  -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
+  -- kernel checking has finished; not all cases are supported yet
+  let (name, info, kind) ← match decl with
+    | .thmDecl thm => pure (thm.name, .thmInfo thm, .thm)
+    | .defnDecl defn => pure (defn.name, .defnInfo defn, .defn)
+    | .mutualDefnDecl [defn] => pure (defn.name, .defnInfo defn, .defn)
+    | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
+    | _ => return (← doAdd)
+
+  -- no environment extension changes to report after kernel checking; ensures we do not
+  -- accidentally wait for this snapshot when querying extension states
+  let async ← env.addConstAsync (reportExts := false) name kind
+  -- report preliminary constant info immediately
+  async.commitConst async.asyncEnv (some info)
+  setEnv async.mainEnv
+  let checkAct ← Core.wrapAsyncAsSnapshot fun _ => do
+    try
+      setEnv async.asyncEnv
+      doAdd
+      async.checkAndCommitEnv (← getEnv)
+    finally
+      async.commitFailure
+  let t ← BaseIO.mapTask (fun _ => checkAct) env.checked
+  let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
+  Core.logSnapshotTask { range? := endRange?, task := t }
+where doAdd := do
   profileitM Exception "type checking" (← getOptions) do
-    let mut env ← withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do
       if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException
-
-    -- register namespaces for newly added constants; this used to be done by the kernel itself
-    -- but that is incompatible with moving it to a separate task
-    env := decl.getNames.foldl registerNamePrefixes env
-    if let .inductDecl _ _ types _ := decl then
-      env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
-    setEnv env
+        logWarning m!"declaration uses 'sorry'"
+      let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
+        |> ofExceptKernelException
+      setEnv env
 
 def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl

src/Lean/CoreM.lean

@@ -515,6 +515,10 @@ register_builtin_option compiler.enableNew : Bool := {
 opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 
 def compileDecl (decl : Declaration) : CoreM Unit := do
+  -- don't compile if kernel errored; should be converted into a task dependency when compilation
+  -- is made async as well
+  if (← get).snapshotTasks.any (·.get.element.diagnostics.msgLog.hasErrors) then
+    return
   let opts ← getOptions
   let decls := Compiler.getDeclNamesForCodeGen decl
   if compiler.enableNew.get opts then
@@ -530,6 +534,10 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
     throwKernelException ex
 
 def compileDecls (decls : List Name) : CoreM Unit := do
+  -- don't compile if kernel errored; should be converted into a task dependency when compilation
+  -- is made async as well
+  if (← get).snapshotTasks.any (·.get.element.diagnostics.msgLog.hasErrors) then
+    return
   let opts ← getOptions
   if compiler.enableNew.get opts then
     compileDeclsNew decls

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -407,8 +407,10 @@ private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType
   let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <|
     mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf
   try
-    let lemmaName ← mkAuxLemma levels expectedType pf
-    return .const lemmaName levelParams
+    -- disable async TC so we can catch its exceptions
+    withOptions (Elab.async.set · false) do
+      let lemmaName ← mkAuxLemma levels expectedType pf
+      return .const lemmaName levelParams
   catch ex =>
     -- Diagnose error
     throwError MessageData.ofLazyM (es := #[expectedType]) do
@@ -473,7 +475,8 @@ where
     -- Level variables occurring in `expectedType`, in ambient order
     let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
     try
-      let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
+      let lemmaName ← withOptions (Elab.async.set · false) do
+        mkAuxLemma lemmaLevels expectedType pf
       return mkConst lemmaName (lemmaLevels.map .param)
     catch _ =>
       diagnose expectedType s none

src/Lean/Meta/IndPredBelow.lean

@@ -591,10 +591,10 @@ def mkBelow (declName : Name) : MetaM Unit := do
       addDecl decl
       trace[Meta.IndPredBelow] "added {ctx.belowNames}"
       ctx.belowNames.forM Lean.mkCasesOn
-      for i in [:ctx.typeInfos.size] do
-        try
           let decl ← IndPredBelow.mkBrecOnDecl ctx i
-          addDecl decl
+          -- disable async TC so we can catch its exceptions
+          withOptions (Elab.async.set · false) do
+            addDecl decl
         catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]!}\n{e.toMessageData}"
     else trace[Meta.IndPredBelow] "Nested or not recursive"
   else trace[Meta.IndPredBelow] "Not inductive predicate"

tests/lean/1027.lean.expected.out

@@ -1,4 +1,4 @@
-1027.lean:1:0-1:7: warning: declaration uses 'sorry'
 x : Nat
 h : ¬x = 0
 ⊢ Unit
+1027.lean:1:0-1:7: warning: declaration uses 'sorry'

tests/lean/1235.lean.expected.out

@@ -1,4 +1,4 @@
-1235.lean:2:0-2:7: warning: declaration uses 'sorry'
 g : Nat → Nat
 h : f 1 = g
 ⊢ g 2 = f 2 1
+1235.lean:2:0-2:7: warning: declaration uses 'sorry'

tests/lean/1681.lean.expected.out

@@ -1,6 +1,6 @@
-1681.lean:1:0-1:7: warning: declaration uses 'sorry'
 x : Nat
 ⊢ Nat
-1681.lean:6:0-6:7: warning: declaration uses 'sorry'
+1681.lean:1:0-1:7: warning: declaration uses 'sorry'
 x : Nat
 ⊢ Nat
+1681.lean:6:0-6:7: warning: declaration uses 'sorry'

tests/lean/1781.lean.expected.out

@@ -2,6 +2,5 @@
   Type ((imax 1 u) + 1)
 but it is expected to have type
   Type (imax 1 u)
-1781.lean:25:12-25:17: error: unknown identifier 'Univ''
-1781.lean:26:15-26:19: error: unknown identifier 'Univ'
-1781.lean:26:8-26:12: error: unknown identifier 'Univ'
+1781.lean:25:4-25:8: error: (kernel) unknown constant 'Univ''
+Univ : Type

tests/lean/1856.lean.expected.out

@@ -1,4 +1,3 @@
-1856.lean:10:4-10:13: warning: declaration uses 'sorry'
 case h
 α : Type ?u
 inst✝ : DecidableEq α
@@ -7,3 +6,4 @@ i : α
 f : (j : α) → β j
 x : α
 ⊢ (if h : x = i then ⋯ ▸ f i else f x) = f x
+1856.lean:10:4-10:13: warning: declaration uses 'sorry'

tests/lean/2505.lean.expected.out

@@ -1,3 +1,3 @@
-2505.lean:14:0-14:7: warning: declaration uses 'sorry'
 target : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
 target' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
+2505.lean:14:0-14:7: warning: declaration uses 'sorry'

tests/lean/690.lean.expected.out

@@ -1,13 +1,13 @@
 690.lean:3:2-3:29: error: too many variable names provided at alternative 'step', #3 provided, but #2 expected
-690.lean:6:0-6:7: warning: declaration uses 'sorry'
 case step
 a b m✝ : Nat
 hStep : a.le m✝
 ih : a.le (m✝ + 1)
 ⊢ a.le (m✝.succ + 1)
-690.lean:11:0-11:7: warning: declaration uses 'sorry'
+690.lean:6:0-6:7: warning: declaration uses 'sorry'
 case step
 a b x : Nat
 hStep : a.le x
 ih : a.le (x + 1)
 ⊢ a.le (x.succ + 1)
+690.lean:11:0-11:7: warning: declaration uses 'sorry'

tests/lean/973b.lean.expected.out

@@ -1,5 +1,5 @@
 973b.lean:5:8-5:10: warning: declaration uses 'sorry'
-973b.lean:9:8-9:11: warning: declaration uses 'sorry'
 [Meta.Tactic.simp.discharge] ex discharge ❌️
       ?p x
 [Meta.Tactic.simp.discharge] ex discharge ❌️ ?p (f x)
+973b.lean:9:8-9:11: warning: declaration uses 'sorry'

tests/lean/consumePPHint.lean.expected.out

@@ -1,6 +1,6 @@
 consumePPHint.lean:4:8-4:14: warning: declaration uses 'sorry'
-consumePPHint.lean:6:8-6:15: warning: declaration uses 'sorry'
 case a
 ⊢ q
     (let_fun x := 0;
     x + 1)
+consumePPHint.lean:6:8-6:15: warning: declaration uses 'sorry'

tests/lean/convInConv.lean.expected.out

@@ -6,7 +6,6 @@ x : Nat
 | x
 x : Nat
 | id (twice x)
-convInConv.lean:15:8-15:12: warning: declaration uses 'sorry'
 y : Nat
 | (fun x => x + y = 0) = fun x => False
 y : Nat
@@ -18,3 +17,4 @@ y : Nat
 | (fun x => y + x = 0) = fun x => False
 y : Nat
 ⊢ (fun x => y + x = 0) = fun x => False
+convInConv.lean:15:8-15:12: warning: declaration uses 'sorry'

tests/lean/inductionGen.lean.expected.out

@@ -1,6 +1,5 @@
 inductionGen.lean:23:2-23:14: error: index in target's type is not a variable (consider using the `cases` tactic instead)
   n + 1
-inductionGen.lean:25:8-25:11: warning: declaration uses 'sorry'
 case cons
 α : Type u_1
 n : Nat
@@ -9,7 +8,7 @@ x : α
 xs : Vec α n
 h : Vec.cons x xs = ys
 ⊢ (Vec.cons x xs).head = ys.head
-inductionGen.lean:64:8-64:11: warning: declaration uses 'sorry'
+inductionGen.lean:25:8-25:11: warning: declaration uses 'sorry'
 case natVal
 α : ExprType
 a✝ : Nat
@@ -41,5 +40,6 @@ a_ih✝ : ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval
 b : Expr ExprType.nat
 h : a✝¹.add a✝ = b
 ⊢ eval (constProp (a✝¹.add a✝)) = eval b
+inductionGen.lean:64:8-64:11: warning: declaration uses 'sorry'
 inductionGen.lean:78:2-78:27: error: target (or one of its indices) occurs more than once
   n

tests/lean/introLetBug.lean.expected.out

@@ -1,4 +1,3 @@
-introLetBug.lean:2:0-2:7: warning: declaration uses 'sorry'
 k : Nat
 this : f 10 = 11
 x : Nat := 10
@@ -7,3 +6,4 @@ k : Nat
 this : f 10 = 11
 ⊢ let x := 10;
   11 = k
+introLetBug.lean:2:0-2:7: warning: declaration uses 'sorry'

tests/lean/renameI.lean.expected.out

@@ -1,9 +1,9 @@
-renameI.lean:1:0-1:7: warning: declaration uses 'sorry'
 x y : Nat
 ⊢ x = y
-renameI.lean:7:0-7:7: warning: declaration uses 'sorry'
+renameI.lean:1:0-1:7: warning: declaration uses 'sorry'
 x a.b : Nat
 ⊢ x = a.b
-renameI.lean:13:0-13:7: warning: declaration uses 'sorry'
+renameI.lean:7:0-7:7: warning: declaration uses 'sorry'
 x o✝ y a.b : Nat
 ⊢ x + y = a.b + o✝
+renameI.lean:13:0-13:7: warning: declaration uses 'sorry'

tests/lean/run/1234.lean

@@ -7,15 +7,15 @@ set_option trace.Meta.Tactic.simp true
 
 
 /--
-warning: declaration uses 'sorry'
----
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
 [Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
 [Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
 [Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
 [Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -32,15 +32,15 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
 -- it works
 
 /--
-warning: declaration uses 'sorry'
----
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
 [Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
 [Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
 [Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
 [Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -55,15 +55,15 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
     ]
 
 /--
-warning: declaration uses 'sorry'
----
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
 [Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
 [Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
 [Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
 [Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):

tests/lean/run/1697.lean

@@ -8,20 +8,19 @@ is false
 #eval show Nat from False.elim (by decide)
 
 /--
-warning: declaration uses 'sorry'
----
-error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to
-runtime instability and crashes.
+error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
 
 To attempt to evaluate anyway despite the risks, use the '#eval!' command.
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 #eval #[1,2,3][2]'sorry
 
 /--
-warning: declaration uses 'sorry'
----
 info: 3
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 #eval! #[1,2,3][2]'sorry

tests/lean/run/2159.lean

@@ -1,9 +1,9 @@
 /--
-warning: declaration uses 'sorry'
----
 info: ⊢ 1.2 < 2
 ---
 info: ⊢ 1.2 < 2
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example : 1.2 < 2 := by