From 442ef6e64cacbae605255676d61d40a8a99a3675 Mon Sep 17 00:00:00 2001 From: jrr6 <7482866+jrr6@users.noreply.github.com> Date: Wed, 16 Jul 2025 23:22:30 -0400 Subject: [PATCH] feat: add case name hints (#9316) This PR adds clickable code-action hints to the "invalid case name" error message. --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 40 +++++++--- tests/lean/caseSuggestions.lean | 10 +++ tests/lean/caseSuggestions.lean.expected.out | 82 +++++++++++--------- tests/lean/run/allGoals.lean | 10 ++- 4 files changed, 90 insertions(+), 52 deletions(-) diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index b8de6dcd5b..d76c6dd21f 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Lean.Meta.Diagnostics +import Lean.Meta.Hint import Lean.Meta.Tactic.Apply import Lean.Meta.Tactic.Assumption import Lean.Meta.Tactic.Contradiction @@ -498,9 +499,9 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do let gs ← getUnsolvedGoals - let g ← if let `(binderIdent| $tag:ident) := tag then - let tag := tag.getId.eraseMacroScopes - let some g ← findTag? gs tag | notFound gs tag + let g ← if let `(binderIdent| $tagId:ident) := tag then + let tagId := tagId.getId.eraseMacroScopes + let some g ← findTag? gs tagId | notFound gs tagId tag pure g else getMainGoal @@ -509,22 +510,31 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List where -- When the case tag is not found, construct a message that tells -- the user what they could have written - notFound (available : List MVarId) (tag : Name) := do + notFound (available : List MVarId) (tag : Name) (tagStx : TSyntax ``binderIdent) := do let firstLine := m!"Case tag {showTagName tag} not found." + let isOriginalStx := tagStx.raw.getHeadInfo matches .original .. -- We must filter out the anonymous name because there may be an -- anonymous goal, but users shouldn't be mistakenly encouraged -- to write `case anonymous` - match (← available.mapM getUserName).filter (· ≠ Name.anonymous) with - | [] => - throwError "{firstLine}\n\nThere are no cases to select." - | [availableName] => - throwError "{firstLine}\n\nThe only available case tag is {showTagName availableName}." - | availableNames => - throwError "Case tag {showTagName tag} not found.\n\nAvailable tags:{commaList <| availableNames.map showTagName}" + let hint ← match (← available.mapM getUserName).filter (· ≠ Name.anonymous) with + | [] => pure <| MessageData.note m!"There are no cases to select." + | [availableName] => + let msg := m!"The only available case tag is {showTagName availableName}." + if isOriginalStx then + MessageData.hint msg (mkSuggestions #[availableName]) (ref? := tagStx) + else + pure <| MessageData.hint' msg + | availableNames => + let msg := "Available tags:" + if isOriginalStx then + MessageData.hint msg (mkSuggestions availableNames.toArray) (ref? := tagStx) + else + pure <| MessageData.hint' m!"{msg}{commaList <| availableNames.map showTagName}" + throwError firstLine ++ hint getUserName (mv : MVarId) := do return (← mv.getDecl).userName - showTagName (tagName : Name) : MessageData := m!"'{tagName}'" + showTagName (tagName : Name) : MessageData := m!"`{tagName}`" -- Construct a comma-separated list that renders one per line, -- indented, if it's too long @@ -533,6 +543,12 @@ where .group <| .nest 2 <| .ofFormat .line ++ .joinSep items sep + mkSuggestions (names : Array Name) := + names.map fun name => + { suggestion := name.toString + toCodeActionTitle? := some fun s => s!"Change case name: {s}" + preInfo? := if names.size == 1 then none else s!"`{name}`: " : Hint.Suggestion } + @[builtin_tactic «case», builtin_incremental] def evalCase : Tactic | stx@`(tactic| case%$caseTk $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) => diff --git a/tests/lean/caseSuggestions.lean b/tests/lean/caseSuggestions.lean index fca6d7c5be..9893b365fd 100644 --- a/tests/lean/caseSuggestions.lean +++ b/tests/lean/caseSuggestions.lean @@ -43,3 +43,13 @@ def sixteenCases : Nat := by cases true <;> cases true <;> cases true <;> cases true case nonexistent => skip + +/-! + This example tests that the code-action hint doesn't appear when the identifier syntax is + synthetic. +-/ +macro "faulty_case_selector " " => " ts:tacticSeq : tactic => `(tactic| case nonexistent => $ts) +def inapplicableSyntax : Nat := by + cases true + faulty_case_selector => + skip diff --git a/tests/lean/caseSuggestions.lean.expected.out b/tests/lean/caseSuggestions.lean.expected.out index eb7b2cb2cc..bdaedadbd7 100644 --- a/tests/lean/caseSuggestions.lean.expected.out +++ b/tests/lean/caseSuggestions.lean.expected.out @@ -1,42 +1,52 @@ -caseSuggestions.lean:11:2-12:8: error: Case tag 'nonexistent' not found. +caseSuggestions.lean:11:2-12:8: error: Case tag `nonexistent` not found. -There are no cases to select. -caseSuggestions.lean:20:2-21:8: error: Case tag 'nonexistent' not found. +Note: There are no cases to select. +caseSuggestions.lean:20:2-21:8: error: Case tag `nonexistent` not found. -The only available case tag is 'unit'. -caseSuggestions.lean:29:2-30:8: error: Case tag 'nonexistent' not found. +Hint: The only available case tag is `unit`. + n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵u̲n̲i̲t̲ +caseSuggestions.lean:29:2-30:8: error: Case tag `nonexistent` not found. -Available tags: 'false', 'true' -caseSuggestions.lean:34:2-35:8: error: Case tag 'nonexistent' not found. +Hint: Available tags: + • `false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲ + • `true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲ +caseSuggestions.lean:34:2-35:8: error: Case tag `nonexistent` not found. -Available tags: 'false.false', 'false.true', 'true.false', 'true.true' -caseSuggestions.lean:39:2-40:8: error: Case tag 'nonexistent' not found. +Hint: Available tags: + • `false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲ +caseSuggestions.lean:39:2-40:8: error: Case tag `nonexistent` not found. -Available tags: - 'false.false.false', - 'false.false.true', - 'false.true.false', - 'false.true.true', - 'true.false.false', - 'true.false.true', - 'true.true.false', - 'true.true.true' -caseSuggestions.lean:44:2-45:8: error: Case tag 'nonexistent' not found. +Hint: Available tags: + • `false.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `false.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `false.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `false.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲ + • `true.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `true.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `true.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `true.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲ +caseSuggestions.lean:44:2-45:8: error: Case tag `nonexistent` not found. -Available tags: - 'false.false.false.false', - 'false.false.false.true', - 'false.false.true.false', - 'false.false.true.true', - 'false.true.false.false', - 'false.true.false.true', - 'false.true.true.false', - 'false.true.true.true', - 'true.false.false.false', - 'true.false.false.true', - 'true.false.true.false', - 'true.false.true.true', - 'true.true.false.false', - 'true.true.false.true', - 'true.true.true.false', - 'true.true.true.true' +Hint: Available tags: + • `false.false.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `false.false.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `false.false.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `false.false.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲ + • `false.true.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `false.true.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `false.true.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `false.true.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲ + • `true.false.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `true.false.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `true.false.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `true.false.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲ + • `true.true.false.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲f̲a̲l̲s̲e̲ + • `true.true.false.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲.̲t̲r̲u̲e̲ + • `true.true.true.false`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲f̲a̲l̲s̲e̲ + • `true.true.true.true`: n̵o̵n̵e̵x̵i̵s̵t̵e̵n̵t̵t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲.̲t̲r̲u̲e̲ +caseSuggestions.lean:54:2-55:8: error: Case tag `nonexistent` not found. + +Hint: Available tags: `false`, `true` diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index 102d142b9b..db22edda44 100644 --- a/tests/lean/run/allGoals.lean +++ b/tests/lean/run/allGoals.lean @@ -141,13 +141,15 @@ even though the metavariable is assigned in the `refine_2.false` case before the -/ set_option pp.mvars false in /-- -error: Case tag 'true' not found. +error: Case tag `true` not found. -The only available case tag is 'refine_2.false'. +Hint: The only available case tag is `refine_2.false`. + t̵r̵u̵e̵r̲e̲f̲i̲n̲e̲_̲2̲.̲f̲a̲l̲s̲e̲ --- -error: Case tag 'true' not found. +error: Case tag `true` not found. -The only available case tag is 'refine_1'. +Hint: The only available case tag is `refine_1`. + t̵r̵u̵e̵r̲e̲f̲i̲n̲e̲_̲1̲ --- trace: case refine_2.false v : Unit := ()