feat: asynchronous kernel checking

src/Lean/AddDecl.lean

@@ -50,18 +50,49 @@ where go env
   | _        => env
 
 def addDecl (decl : Declaration) : CoreM Unit := do
-  profileitM Exception "type checking" (← getOptions) do
-    let mut env ← withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
-      if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException
+  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
 
-    -- 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
     setEnv env
+    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)
+    | _ => 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.commitCheckEnv (← 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
+    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        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

@@ -522,6 +522,10 @@ opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment
 
 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 !decl.getNames.all (← getEnv).constants.contains then
+    return
   let opts ← getOptions
   let decls := Compiler.getDeclNamesForCodeGen decl
   if compiler.enableNew.get opts then
@@ -537,6 +541,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 !decls.all (← getEnv).constants.contains then
+    return
   let opts ← getOptions
   if compiler.enableNew.get opts then
     compileDeclsNew decls

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -308,7 +308,7 @@ def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
       throwError (← addMessageContextFull errorMessage)
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
-def evalBvTrace : Tactic := fun
+def evalBvDecide : Tactic := fun
   | `(tactic| bv_decide $cfg:optConfig) => do
     let cfg ← elabBVDecideConfig cfg
     IO.FS.withTempFile fun _ lratFile => do
@@ -319,4 +319,3 @@ def evalBvTrace : Tactic := fun
 
 end Frontend
 end Lean.Elab.Tactic.BVDecide
-

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -197,8 +197,10 @@ def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContex
       (← mkEqRefl (toExpr true))
   try
     let auxLemma ←
-      withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
-        mkAuxLemma [] auxType auxProof
+      -- disable async TC so we can catch its exceptions
+      withOptions (Elab.async.set · false) do
+        withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
+          mkAuxLemma [] auxType auxProof
     return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
   catch e =>
     throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"

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

@@ -594,7 +594,9 @@ def mkBelow (declName : Name) : MetaM Unit := do
       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"

src/library/compiler/ir_interpreter.cpp

@@ -812,7 +812,7 @@ private:
     decl get_decl(name const & fn) {
         option_ref<decl> d = find_ir_decl(m_env, fn);
         if (!d) {
-            throw exception(sstream() << "unknown declaration '" << fn << "'");
+            throw exception(sstream() << "(interpreter) unknown declaration '" << fn << "'");
         }
         return d.get().value();
     }

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 @@
+x : Nat
+⊢ Nat
 1681.lean:1:0-1:7: warning: declaration uses 'sorry'
 x : Nat
 ⊢ Nat
 1681.lean:6:0-6:7: warning: declaration uses 'sorry'
-x : Nat
-⊢ Nat

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,8 +7,6 @@ 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
@@ -16,6 +14,8 @@ info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> 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,8 +32,6 @@ 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
@@ -41,6 +39,8 @@ info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> 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,8 +55,6 @@ 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
@@ -64,6 +62,8 @@ info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> 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 @@
 /--
+info: ⊢ 1.2 < 2
+---
+info: ⊢ 1.2 < 2
+---
 warning: declaration uses 'sorry'
----
-info: ⊢ 1.2 < 2
----
-info: ⊢ 1.2 < 2
 -/
 #guard_msgs in
 example : 1.2 < 2 := by

tests/lean/run/2916.lean

@@ -1,10 +1,10 @@
 set_option pp.coercions false -- Show `OfNat.ofNat` when present for clarity
 
 /--
-warning: declaration uses 'sorry'
----
 info: x : Nat
 ⊢ OfNat.ofNat 2 = x
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example : nat_lit 2 = x := by
@@ -13,10 +13,10 @@ example : nat_lit 2 = x := by
   sorry
 
 /--
-warning: declaration uses 'sorry'
----
 info: x : Nat
 ⊢ OfNat.ofNat 2 = x
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example : nat_lit 2 = x := by
@@ -25,12 +25,12 @@ example : nat_lit 2 = x := by
   sorry
 
 /--
-warning: declaration uses 'sorry'
----
 info: α : Nat → Type
 f : (n : Nat) → α n
 x : α (OfNat.ofNat 2)
 ⊢ f (OfNat.ofNat 2) = x
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (α : Nat → Type) (f : (n : Nat) → α n) (x : α 2) : f (nat_lit 2) = x := by
@@ -57,8 +57,6 @@ example (f : Nat → Nat) (h : f 2 = x) : f 2 = x := by
   assumption
 
 /--
-warning: declaration uses 'sorry'
----
 info: α : Nat → Type
 f : (n : Nat) → α n
 x : α (OfNat.ofNat 2)
@@ -68,6 +66,8 @@ info: α : Nat → Type
 f : (n : Nat) → α n
 x : α (OfNat.ofNat 2)
 ⊢ f 2 = x
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (α : Nat → Type) (f : (n : Nat) → α n) (x : α 2) : f 2 = x := by

tests/lean/run/compiler_proj_bug.lean

@@ -5,9 +5,9 @@ def f (s : S) :=
 s.b - s.a
 
 /--
-warning: declaration uses 'sorry'
----
 info: 25
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 #eval! f {a := 5, b := 30, h := sorry }

tests/lean/run/dsimp_bv_simproc.lean

@@ -10,13 +10,13 @@ theorem write_simplify_test_0 (a x y : BitVec 64)
   simp only [setWidth_eq, BitVec.cast_eq]
 
 /--
-warning: declaration uses 'sorry'
----
 info: write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type
 s aux : Type
 a x y : BitVec 64
 h : 128 = 128
 ⊢ write 16 a (x ++ y) s = aux
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (a x y : BitVec 64)

tests/lean/run/ext.lean

@@ -150,11 +150,11 @@ More informative error (issue #4758)
 -/
 
 /--
-warning: declaration uses 'sorry'
----
 error: Failed to generate an 'ext_iff' theorem from 'weird_prod_ext': argument f is not a proof, which is not supported for arguments after p and q
 
 Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 @[ext]

tests/lean/run/generalizeMany.lean

@@ -1,8 +1,6 @@
 set_option pp.analyze false
 
 /--
-warning: declaration uses 'sorry'
----
 info: p : (n : Nat) → Fin n → Prop
 n : Nat
 v : Fin n
@@ -11,6 +9,8 @@ v' : Fin n'
 h₁ : n + 1 = n'
 h₂ : HEq v.succ v'
 ⊢ p n' v'
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (p : (n : Nat) → Fin n → Prop)

tests/lean/run/grind_pattern2.lean

@@ -45,8 +45,6 @@ grind_pattern fooThm => foo x [a, b]
 
 
 /--
-warning: declaration uses 'sorry'
----
 info: [grind.internalize] foo x y
 [grind.internalize] [a, b]
 [grind.internalize] Nat
@@ -58,6 +56,8 @@ info: [grind.internalize] foo x y
 [grind.internalize] x
 [grind.internalize] y
 [grind.internalize] z
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 set_option trace.grind.internalize true in

tests/lean/run/grind_pre.lean

@@ -187,13 +187,13 @@ example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h
   grind
 
 /--
-warning: declaration uses 'sorry'
----
 info: [grind.issues] found congruence between
       g b
     and
       f a
     but functions have different types
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 set_option trace.grind.issues true in

tests/lean/run/inliner_loop.lean

@@ -1,5 +1,3 @@
-
-
 unsafe inductive t
 | mk : (t → t) → t
 

tests/lean/run/lazyListRotateUnfoldProof.lean

@@ -42,8 +42,6 @@ def LazyList.ind {α : Type u} {motive : LazyList α → Sort v}
 -- Remark: Lean used well-founded recursion behind the scenes to define LazyList.ind
 
 /--
-warning: declaration uses 'sorry'
----
 info: case cons
 τ : Type u_1
 nil : LazyList τ
@@ -62,6 +60,8 @@ t : Thunk (LazyList τ)
 a✝ : ∀ (h : t.get.length + 1 = R.length), (rotate t.get R nil h).length = t.get.length + R.length
 ⊢ ∀ (h : (LazyList.delayed t).length + 1 = R.length),
     (rotate (LazyList.delayed t) R nil h).length = (LazyList.delayed t).length + R.length
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 theorem rotate_inv' {F : LazyList τ} {R : List τ} : (h : F.length + 1 = R.length) → (rotate F R nil h).length = F.length + R.length := by

tests/lean/run/safeExp.lean

@@ -19,13 +19,13 @@ example : 2^257 = 2*2^256 :=
 /--
 warning: exponent 2008 exceeds the threshold 256, exponentiation operation was not evaluated, use `set_option exponentiation.threshold <num>` to set a new threshold
 ---
-warning: declaration uses 'sorry'
----
-error: (kernel) deep recursion detected
----
 info: k : Nat
 h : k = 2008 ^ 2 + 2 ^ 2008
 ⊢ ((4032064 + 2 ^ 2008) ^ 2 + 2 ^ (4032064 + 2 ^ 2008)) % 10 = 6
+---
+warning: declaration uses 'sorry'
+---
+error: (kernel) deep recursion detected
 -/
 #guard_msgs in
 example (k : Nat) (h : k = 2008^2 + 2^2008) : (k^2 + 2^k)%10 = 6 := by
@@ -34,11 +34,11 @@ example (k : Nat) (h : k = 2008^2 + 2^2008) : (k^2 + 2^k)%10 = 6 := by
   sorry
 
 /--
-warning: declaration uses 'sorry'
----
 info: k : Nat
 h : k = 2008 ^ 2 + 2 ^ 2008
 ⊢ ((2008 ^ 2 + 2 ^ 2008) ^ 2 + 2 ^ (2008 ^ 2 + 2 ^ 2008)) % 10 = 6
+---
+warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (k : Nat) (h : k = 2008^2 + 2^2008) : (k^2 + 2^k)%10 = 6 := by

tests/lean/rwWithoutOffsetCnstrs.lean.expected.out

@@ -1,3 +1,3 @@
-rwWithoutOffsetCnstrs.lean:5:0-5:7: warning: declaration uses 'sorry'
 m n : Nat
 ⊢ (n + 1).ble n = false
+rwWithoutOffsetCnstrs.lean:5:0-5:7: warning: declaration uses 'sorry'

tests/lean/simp_dsimp.lean.expected.out

@@ -1,8 +1,8 @@
-simp_dsimp.lean:4:0-4:7: warning: declaration uses 'sorry'
 x : Nat
 a : A (x + 0)
 ⊢ f x a = x
-simp_dsimp.lean:9:0-9:7: warning: declaration uses 'sorry'
+simp_dsimp.lean:4:0-4:7: warning: declaration uses 'sorry'
 x : Nat
 a : A (x + 0)
 ⊢ f (x + 0) a = x
+simp_dsimp.lean:9:0-9:7: warning: declaration uses 'sorry'

tests/lean/simp_trace.lean.expected.out

@@ -61,9 +61,9 @@ Try this: simp only [my_thm]
 [Meta.Tactic.simp.rewrite] my_thm:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] eq_self:1000, (a ∧ b) = (a ∧ b) ==> True
 Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
-simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
 [Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
 [Meta.Tactic.simp.rewrite] eq_self:1000, x = x ==> True
+simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z

tests/lean/unfoldDefEq.lean.expected.out

@@ -1,4 +1,3 @@
-unfoldDefEq.lean:7:0-7:7: warning: declaration uses 'sorry'
 n : Nat
 x : (Fin n, Fin n).fst
 h : some_property x
@@ -7,8 +6,9 @@ n : Nat
 x : Fin n
 h : some_property x
 ⊢ True
-unfoldDefEq.lean:14:0-14:7: warning: declaration uses 'sorry'
+unfoldDefEq.lean:7:0-7:7: warning: declaration uses 'sorry'
 n : Nat
 x : Fin n
 h : some_property x
 ⊢ True
+unfoldDefEq.lean:14:0-14:7: warning: declaration uses 'sorry'

tests/lean/unfoldReduceMatch.lean.expected.out

@@ -1,3 +1,3 @@
-unfoldReduceMatch.lean:2:0-2:7: warning: declaration uses 'sorry'
 n : Nat
 ⊢ (zero.add n).succ = n.succ
+unfoldReduceMatch.lean:2:0-2:7: warning: declaration uses 'sorry'