feat: add option debug.byAsSorry true (#4576)

src/Lean/Elab/BuiltinTerm.lean

@@ -157,9 +157,19 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
+register_builtin_option debug.byAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
+}
+
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
-  | some expectedType => mkTacticMVar expectedType stx
+  | some expectedType =>
+    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
+      mkSorry expectedType false
+    else
+      mkTacticMVar expectedType stx
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

tests/lean/run/byAsSorry.lean

@@ -0,0 +1,30 @@
+set_option debug.byAsSorry true in
+/--
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+theorem ex1 (h : b = a) : a = b := by
+  rw [h]
+
+/--
+-/
+#guard_msgs in
+theorem ex2 (h : b = a) : a = b := by
+  rw [h]
+
+set_option debug.byAsSorry true in
+/-- -/
+#guard_msgs in
+def f (x : Nat) : Nat := by
+  exact x + 1 -- must not become a sorry since expected type is data
+
+set_option debug.byAsSorry true in
+/--
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+def g (x : Nat) : { x : Nat // x > 0 } :=
+  ⟨by exact x + 1, by omega⟩
+
+example : (g x).1 = x + 1 := by
+  rfl