From 49d5cf6d7a8c9f2838b0f34827a2c7e413341955 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 2 Dec 2024 17:41:47 +0100 Subject: [PATCH] feat: asynchronous kernel checking --- src/Lean/AddDecl.lean | 51 +++++++++++++++---- src/Lean/CoreM.lean | 8 +++ .../Tactic/BVDecide/Frontend/BVDecide.lean | 3 +- .../Elab/Tactic/BVDecide/Frontend/LRAT.lean | 6 ++- src/Lean/Elab/Tactic/ElabTerm.lean | 9 ++-- src/Lean/Meta/IndPredBelow.lean | 4 +- src/library/compiler/ir_interpreter.cpp | 2 +- tests/lean/1027.lean.expected.out | 2 +- tests/lean/1235.lean.expected.out | 2 +- tests/lean/1681.lean.expected.out | 4 +- tests/lean/1781.lean.expected.out | 5 +- tests/lean/1856.lean.expected.out | 2 +- tests/lean/2505.lean.expected.out | 2 +- tests/lean/690.lean.expected.out | 4 +- tests/lean/973b.lean.expected.out | 2 +- tests/lean/consumePPHint.lean.expected.out | 2 +- tests/lean/convInConv.lean.expected.out | 2 +- tests/lean/inductionGen.lean.expected.out | 4 +- tests/lean/introLetBug.lean.expected.out | 2 +- tests/lean/renameI.lean.expected.out | 6 +-- tests/lean/run/1234.lean | 12 ++--- tests/lean/run/1697.lean | 11 ++-- tests/lean/run/2159.lean | 4 +- tests/lean/run/2916.lean | 16 +++--- tests/lean/run/compiler_proj_bug.lean | 4 +- tests/lean/run/dsimp_bv_simproc.lean | 4 +- tests/lean/run/ext.lean | 4 +- tests/lean/run/generalizeMany.lean | 4 +- tests/lean/run/grind_pattern2.lean | 4 +- tests/lean/run/grind_pre.lean | 4 +- tests/lean/run/inliner_loop.lean | 2 - tests/lean/run/lazyListRotateUnfoldProof.lean | 4 +- tests/lean/run/safeExp.lean | 12 ++--- .../rwWithoutOffsetCnstrs.lean.expected.out | 2 +- tests/lean/simp_dsimp.lean.expected.out | 4 +- tests/lean/simp_trace.lean.expected.out | 2 +- tests/lean/unfoldDefEq.lean.expected.out | 4 +- .../lean/unfoldReduceMatch.lean.expected.out | 2 +- 38 files changed, 131 insertions(+), 90 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 7a8c7876c8fe5..1a1a86e92b7f1 100644 --- a/src/Lean/AddDecl.lean +++ b/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 diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 7fc6e9683c583..f5f1244ad6a47 100644 --- a/src/Lean/CoreM.lean +++ b/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).toKernelEnv.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).toKernelEnv.constants.contains then + return let opts ← getOptions if compiler.enableNew.get opts then compileDeclsNew decls diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 6466e8ee9bdca..bf5bec71de798 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/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 - diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean index 01f8bfc793aa0..7178e12d43983 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean +++ b/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}" diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 0a412ae3f1bef..a599dfc05b00e 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/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 diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index cfb96e6abb455..b355414a662bb 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/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" diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 2f32ef8621503..17f0742eac561 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -812,7 +812,7 @@ class interpreter { decl get_decl(name const & fn) { option_ref 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(); } diff --git a/tests/lean/1027.lean.expected.out b/tests/lean/1027.lean.expected.out index 073b4e229999f..2a535e3f5ca1f 100644 --- a/tests/lean/1027.lean.expected.out +++ b/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' diff --git a/tests/lean/1235.lean.expected.out b/tests/lean/1235.lean.expected.out index aa7dcb6381508..f052d64906b62 100644 --- a/tests/lean/1235.lean.expected.out +++ b/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' diff --git a/tests/lean/1681.lean.expected.out b/tests/lean/1681.lean.expected.out index bad4ebe7cc0c8..4c531997633ff 100644 --- a/tests/lean/1681.lean.expected.out +++ b/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' diff --git a/tests/lean/1781.lean.expected.out b/tests/lean/1781.lean.expected.out index d862f4630071c..766e1f5dc74ea 100644 --- a/tests/lean/1781.lean.expected.out +++ b/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 diff --git a/tests/lean/1856.lean.expected.out b/tests/lean/1856.lean.expected.out index afefbff9393ff..66a213757486a 100644 --- a/tests/lean/1856.lean.expected.out +++ b/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' diff --git a/tests/lean/2505.lean.expected.out b/tests/lean/2505.lean.expected.out index 98a7adec30c0f..6610d40a35441 100644 --- a/tests/lean/2505.lean.expected.out +++ b/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' diff --git a/tests/lean/690.lean.expected.out b/tests/lean/690.lean.expected.out index e0cde260b0ebf..78f576cd2f282 100644 --- a/tests/lean/690.lean.expected.out +++ b/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' diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out index 0cd8213d49b1f..249335fe41cdc 100644 --- a/tests/lean/973b.lean.expected.out +++ b/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' diff --git a/tests/lean/consumePPHint.lean.expected.out b/tests/lean/consumePPHint.lean.expected.out index 87ec714a78254..ff65105109bfb 100644 --- a/tests/lean/consumePPHint.lean.expected.out +++ b/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' diff --git a/tests/lean/convInConv.lean.expected.out b/tests/lean/convInConv.lean.expected.out index d27c28c38e4ad..9a2e6261add8a 100644 --- a/tests/lean/convInConv.lean.expected.out +++ b/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' diff --git a/tests/lean/inductionGen.lean.expected.out b/tests/lean/inductionGen.lean.expected.out index 6c28bbba21937..a9d17f9194d8a 100644 --- a/tests/lean/inductionGen.lean.expected.out +++ b/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 diff --git a/tests/lean/introLetBug.lean.expected.out b/tests/lean/introLetBug.lean.expected.out index 4adc2fa3588b4..adb19d6d47c2e 100644 --- a/tests/lean/introLetBug.lean.expected.out +++ b/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' diff --git a/tests/lean/renameI.lean.expected.out b/tests/lean/renameI.lean.expected.out index 4296230e39c21..9ef5f3596f08c 100644 --- a/tests/lean/renameI.lean.expected.out +++ b/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' diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean index 825378b8cd628..7ae93d41e4bb4 100644 --- a/tests/lean/run/1234.lean +++ b/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): diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean index 7f0013e2c2f7d..d56d803339f25 100644 --- a/tests/lean/run/1697.lean +++ b/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 diff --git a/tests/lean/run/2159.lean b/tests/lean/run/2159.lean index ee43bd5afdc82..4c51b3ada4de4 100644 --- a/tests/lean/run/2159.lean +++ b/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 diff --git a/tests/lean/run/2916.lean b/tests/lean/run/2916.lean index f90249abe8434..45716a7faa70a 100644 --- a/tests/lean/run/2916.lean +++ b/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 diff --git a/tests/lean/run/compiler_proj_bug.lean b/tests/lean/run/compiler_proj_bug.lean index a21dd71b823fb..90c13d592220a 100644 --- a/tests/lean/run/compiler_proj_bug.lean +++ b/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 } diff --git a/tests/lean/run/dsimp_bv_simproc.lean b/tests/lean/run/dsimp_bv_simproc.lean index 4951feee5371a..90560ac72beeb 100644 --- a/tests/lean/run/dsimp_bv_simproc.lean +++ b/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) diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean index 36906a67a3118..3c513dccbf797 100644 --- a/tests/lean/run/ext.lean +++ b/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] diff --git a/tests/lean/run/generalizeMany.lean b/tests/lean/run/generalizeMany.lean index 98ae6f2649c57..d83050742953d 100644 --- a/tests/lean/run/generalizeMany.lean +++ b/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) diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean index 8d061b72ac14a..8e0db05208be5 100644 --- a/tests/lean/run/grind_pattern2.lean +++ b/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 diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean index 06ce0af8bca0d..fa5c9df47dd9e 100644 --- a/tests/lean/run/grind_pre.lean +++ b/tests/lean/run/grind_pre.lean @@ -212,13 +212,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 diff --git a/tests/lean/run/inliner_loop.lean b/tests/lean/run/inliner_loop.lean index d95128c84c090..0feb7c37cb369 100644 --- a/tests/lean/run/inliner_loop.lean +++ b/tests/lean/run/inliner_loop.lean @@ -1,5 +1,3 @@ - - unsafe inductive t | mk : (t → t) → t diff --git a/tests/lean/run/lazyListRotateUnfoldProof.lean b/tests/lean/run/lazyListRotateUnfoldProof.lean index 097d45e4c59a2..b09a971709eb4 100644 --- a/tests/lean/run/lazyListRotateUnfoldProof.lean +++ b/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 diff --git a/tests/lean/run/safeExp.lean b/tests/lean/run/safeExp.lean index ef27868f32051..ec9986fb78fa3 100644 --- a/tests/lean/run/safeExp.lean +++ b/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 ` 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 diff --git a/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out b/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out index 2a442e29993c3..b877c1b27ee09 100644 --- a/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out +++ b/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' diff --git a/tests/lean/simp_dsimp.lean.expected.out b/tests/lean/simp_dsimp.lean.expected.out index 9a84165273372..75c47b01d9538 100644 --- a/tests/lean/simp_dsimp.lean.expected.out +++ b/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' diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out index 9894b0558c98e..85364280484a5 100644 --- a/tests/lean/simp_trace.lean.expected.out +++ b/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 diff --git a/tests/lean/unfoldDefEq.lean.expected.out b/tests/lean/unfoldDefEq.lean.expected.out index d1da836d83572..aff2cacafb622 100644 --- a/tests/lean/unfoldDefEq.lean.expected.out +++ b/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' diff --git a/tests/lean/unfoldReduceMatch.lean.expected.out b/tests/lean/unfoldReduceMatch.lean.expected.out index 4460afe799d15..efbdd04e527f9 100644 --- a/tests/lean/unfoldReduceMatch.lean.expected.out +++ b/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'