feat: exact?%: do not report suggestions which do not close the goal (

#3974) This makes `exact?%` behave like `by exact?` rather than `by apply?`. If the underlying function `librarySearch` finds a suggestion which closes the goal, use it (and add a code action). Otherwise log an error and use `sorry`. The error is either ```text `exact?%` didn't find any relevant lemmas ``` or ```text `exact?%` could not close the goal. Try `by apply` to see partial suggestions. ``` --- [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Useful.20term.20elaborators/near/434863856) --------- Co-authored-by: Scott Morrison <[email protected]>
leanprover · Apr 24, 2024 · 4fe0259 · 4fe0259
1 parent 41697dc
commit 4fe0259
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 6 deletions.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
@@ -1542,7 +1542,7 @@ macro "get_elem_tactic" : tactic =>
 
 /--
 Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
+for `exact?%` to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
 

diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -68,11 +68,8 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     let (_, introdGoal) ← goal.mvarId!.intros
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
-        reportOutOfHeartbeats `library_search stx
-        for suggestion in suggestions do
-          withMCtx suggestion.2 do
-            addTermSuggestion stx (← instantiateMVars goal).headBeta
-        if suggestions.isEmpty then logError "exact?# didn't find any relevant lemmas"
+        if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
+        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
         mkSorry expectedType (synthetic := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta

diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean
@@ -43,6 +43,14 @@ example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
 #guard_msgs in
 example : x < x + 1 := exact?%
 
+/-- error: `exact?%` didn't find any relevant lemmas -/
+#guard_msgs in
+example {α : Sort u} (x y : α) : Eq x y := exact?%
+
+/-- error: `exact?%` could not close the goal. Try `by apply` to see partial suggestions. -/
+#guard_msgs in
+example (x y : Nat) : x ≤ y := exact?%
+
 /-- info: Try this: exact p -/
 #guard_msgs in
 example (P : Prop) (p : P) : P := by apply?