From 073b2cfc83dbb385548b5e5851e69d0713a578dc Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 21 Jun 2024 17:06:07 +0200 Subject: [PATCH] fix: cdot parser error message range (#4528) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit as #4527 describes there is inconsistency between `by`, `case` and `next` on the one hand who, if the goal isn’t closed, put squiggly underlines on the first line, and `.`, which so far only squiggled the dot (which is a very short symbol!) With this change the same mechanism as used by `case`, namely `withCaseRef`, is also used for `.`. There is an argument for the status quo: The `.` tactic is more commonly used with further tactics on the same line, and thus there is now a higher risk that the user might think that the first tactic is broken. But * the same argument does apply to `by` and `case` where there was an intentional choice to do it this way * consistency and * a squiggly line just under the short `.` is easy to miss, so it is actually better to underlining more here (at least until we have a better way to indicate incomplete proofs, which I have hopes for) Fixes #4527, at least most of it. --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 2 +- tests/lean/interactive/issue4527.lean | 5 +++++ tests/lean/interactive/issue4527.lean.expected.out | 10 ++++++++++ tests/lean/refineFiltersOldMVars.lean.expected.out | 6 +++--- tests/lean/tacUnsolvedGoalsErrors.lean.expected.out | 4 ++-- 5 files changed, 21 insertions(+), 6 deletions(-) create mode 100644 tests/lean/interactive/issue4527.lean create mode 100644 tests/lean/interactive/issue4527.lean.expected.out diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index b6a8739809..883ba7da88 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -199,7 +199,7 @@ def evalTacticCDot : Tactic := fun stx => do -- but the token antiquotation does not copy trailing whitespace, leading to -- differences in the goal display (#2153) let initInfo ← mkInitialTacticInfo stx[0] - withRef stx[0] <| closeUsingOrAdmit do + withCaseRef stx[0] stx[1] <| closeUsingOrAdmit do -- save state before/after entering focus on `·` withInfoContext (pure ()) initInfo Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx diff --git a/tests/lean/interactive/issue4527.lean b/tests/lean/interactive/issue4527.lean new file mode 100644 index 0000000000..407eb42452 --- /dev/null +++ b/tests/lean/interactive/issue4527.lean @@ -0,0 +1,5 @@ +example : True := by + . skip + --^ collectDiagnostics + skip + -- foo diff --git a/tests/lean/interactive/issue4527.lean.expected.out b/tests/lean/interactive/issue4527.lean.expected.out new file mode 100644 index 0000000000..0a542d8842 --- /dev/null +++ b/tests/lean/interactive/issue4527.lean.expected.out @@ -0,0 +1,10 @@ +{"version": 1, + "uri": "file:///issue4527.lean", + "diagnostics": + [{"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 1, "character": 2}, "end": {"line": 2, "character": 0}}, + "message": "unsolved goals\n⊢ True", + "fullRange": + {"start": {"line": 1, "character": 2}, "end": {"line": 3, "character": 8}}}]} diff --git a/tests/lean/refineFiltersOldMVars.lean.expected.out b/tests/lean/refineFiltersOldMVars.lean.expected.out index f0912d5d24..2bdca00e0a 100644 --- a/tests/lean/refineFiltersOldMVars.lean.expected.out +++ b/tests/lean/refineFiltersOldMVars.lean.expected.out @@ -9,12 +9,12 @@ h : Type case a ⊢ Type refineFiltersOldMVars.lean:66:4-66:11: error: no goals to be solved -refineFiltersOldMVars.lean:101:2-101:3: error: unsolved goals +refineFiltersOldMVars.lean:101:2-101:13: error: unsolved goals case d ⊢ Bool -refineFiltersOldMVars.lean:102:2-102:3: error: unsolved goals +refineFiltersOldMVars.lean:102:2-102:13: error: unsolved goals case e ⊢ Nat -refineFiltersOldMVars.lean:109:2-109:3: error: unsolved goals +refineFiltersOldMVars.lean:109:2-109:13: error: unsolved goals case e ⊢ Bool diff --git a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out index 7f6b5a7382..ad43b70d2b 100644 --- a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out +++ b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out @@ -32,13 +32,13 @@ p q r : Prop h2 : p → q h✝ : q ⊢ q -tacUnsolvedGoalsErrors.lean:26:2-26:3: error: unsolved goals +tacUnsolvedGoalsErrors.lean:26:2-27:8: error: unsolved goals case inl p q r : Prop h2 : p → q h✝ : p ⊢ q -tacUnsolvedGoalsErrors.lean:28:2-28:3: error: unsolved goals +tacUnsolvedGoalsErrors.lean:28:2-29:8: error: unsolved goals case inr p q r : Prop h2 : p → q