fix: ensure sorry is available

We want to make sure we can use `debug.proofAsSorry` when compiling Lean.

src/Lean/Elab/MutualDef.lean

@@ -399,6 +399,20 @@ register_builtin_option linter.unusedSectionVars : Bool := {
   descr := "enable the 'unused section variables in theorem body' linter"
 }
 
+register_builtin_option debug.proofAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "replace the bodies (proofs) of theorems with `sorry`"
+}
+
+/-- Returns true if `k` is a theorem, option `debug.proofAsSorry` is set to true, and the environment contains the axiom `sorryAx`. -/
+private def useProofAsSorry (k : DefKind) : CoreM Bool := do
+  if k.isTheorem then
+    if debug.proofAsSorry.get (← getOptions) then
+      if (← getEnv).contains ``sorryAx then
+        return true
+  return false
+
 private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr) (sc : Command.Scope) : TermElabM (Array Expr) :=
   headers.mapM fun header => do
     let mut reusableResult? := none
@@ -420,7 +434,9 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
         for h : i in [0:header.binderIds.size] do
           -- skip auto-bound prefix in `xs`
           addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
-        let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
+        let val ← if (← useProofAsSorry header.kind) then
+          mkSorry type false
+        else withReader ({ · with tacSnap? := header.tacSnap? }) do
           -- Store instantiated body in info tree for the benefit of the unused variables linter
           -- and other metaprograms that may want to inspect it without paying for the instantiation
           -- again

src/stdlib_flags.h

@@ -5,9 +5,8 @@ options get_default_options() {
     options opts;
     // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
-    // set to true to generally avoid bootstrapping issues limited to tactic
-    // blocks in stage 1
-    opts = opts.update({"debug", "byAsSorry"}, false);
+    // set to true to generally avoid bootstrapping issues limited to proofs
+    opts = opts.update({"debug", "proofAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
     opts = opts.update({"interpreter", "prefer_native"}, false);

tests/lean/run/proofAsSorry.lean

@@ -0,0 +1,46 @@
+set_option debug.proofAsSorry true
+
+/--
+error: type mismatch
+  rfl
+has type
+  ?m.156 = ?m.156 : Prop
+but is expected to have type
+  2 + 2 = 5 : Prop
+-/
+#guard_msgs in
+example : 2 + 2 = 5 := rfl -- This is not a theorem
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem ex : 2 + 2 = 5 := rfl
+
+#guard_msgs in
+def data (w : Nat) : String := toString w
+
+/-- info: "37" -/
+#guard_msgs in
+#eval data 37
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem tst1 : 0 + x = 1*x + 0 := by
+  simp
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem tst2 : ∀ x, 0 + x = 1*x + 0 := by
+  intro x
+  simp
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+theorem tst3 : x = 2*x + 1 := by
+  rfl
+
+#guard_msgs in
+def concatSelf (as : List α) := as ++ as
+
+/-- info: [1, 2, 3, 1, 2, 3] -/
+#guard_msgs in
+#eval concatSelf [1, 2, 3]