fix: apply? produces a non-synthetic sorry (#8231)

This PR changes the behaviour of `apply?` so that the `sorry` it uses to
close the goal is non-synthetic. (Recall that correct use of synthetic
sorries requires that the tactic also generates an error message, which
we don't want to do in this situation.) Either this PR or #8230 are
sufficient to defend against the problem reported in #8212.

(cherry picked from commit 77b9e51)

Author: kim-em

src/Lean/Elab/Tactic/Basic.lean

@@ -11,10 +11,10 @@ namespace Lean.Elab
 open Meta
 
 /-- Assign `mvarId := sorry` -/
-def admitGoal (mvarId : MVarId) : MetaM Unit :=
+def admitGoal (mvarId : MVarId) (synthetic : Bool := true): MetaM Unit :=
   mvarId.withContext do
     let mvarType ← inferType (mkMVar mvarId)
-    mvarId.assign (← mkLabeledSorry mvarType (synthetic := true) (unique := true))
+    mvarId.assign (← mkLabeledSorry mvarType (synthetic := synthetic) (unique := true))
 
 def goalsToMessageData (goals : List MVarId) : MessageData :=
   MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -48,7 +48,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
           addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
             (checkState? := initialState) (addSubgoalsMsg := true) (tacticErrorAsInfo := true)
       if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
-      admitGoal goal
+      admitGoal goal (synthetic := false)
 
 @[builtin_tactic Lean.Parser.Tactic.exact?]
 def evalExact : Tactic := fun stx => do

tests/lean/librarySearch.lean

@@ -275,3 +275,7 @@ error: apply? didn't find any relevant lemmas
 -/
 #guard_msgs in
 example {α : Sort u} (x y : α) : Eq x y := by apply?
+
+-- Verify that there is a `sorry` warning when `apply?` closes the goal.
+#guard_msgs (drop info) in
+example : False := by apply?

tests/lean/librarySearch.lean.expected.out

@@ -0,0 +1 @@
+librarySearch.lean:281:0-281:7: warning: declaration uses 'sorry'