From 06fb4bec529131fc93166ddc47eb93c2ffc147b8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 8 Apr 2026 16:05:47 +0200 Subject: [PATCH] feat: require indentation in commands, allow empty tactic sequences (#13229) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR wraps the top-level command parser with `withPosition` to enforce indentation in `by` blocks, combined with an empty-by fallback for better error messages. This subsumes #3215 (which introduced `withPosition commandParser` but without the empty-by fallback). It is also related to #9524, which explores elaboration with empty tactic sequences — this PR reuses that idea for the empty-by fallback, so that a `by` not followed by an indented tactic produces an elaboration error (unsolved goals) rather than a parse error. **Changes:** - `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`, setting the saved position at the start of each top-level command - `tacticSeqIndentGt` gains an empty tactic sequence fallback (`pushNone`) so that missing indentation produces an elaboration error (unsolved goals) instead of a parse error - `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty `by` blocks parse successfully via `pushNone` (producing empty nodes) rather than producing `.missing` syntax, making the `isEmptyBy` check dead code. The `isEmpty` helper in `isSyntheticTacticCompletion` continues to work correctly because it handles both `.missing` and empty nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on `#[]`) - Test files updated to indent `by` blocks and expression continuations that were previously at column 0 **Behavior:** - Top-level `by` blocks now require indentation (column > 0 for commands at column 0) - Commands indented inside `section` require proofs to be indented past the command's column - `#guard_msgs in example : True := by` works because tactic indentation is checked against the outermost command's column - Expression continuations (not just `by`) must also be indented past the command, which is slightly more strict but more consistent - `have : True := by` followed by a dedent now correctly puts `this` in scope in the outer tactic block (the `have` is structurally complete with an unsolved-goal error, rather than a parse error) **Code changes observed in practice (lean4 test suite + Mathlib):** - `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed by tactics at column 0 must be indented - `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}` where the second line starts at column 0 must be indented (most common category in Mathlib) - Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]` where the body/arguments start at column 0 - Structure literals: `.symm\n{ toFun := ...` where the struct literal starts at column 0 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.6 --------- Co-authored-by: Claude Opus 4.6 --- .../Data/Range/Polymorphic/NatLemmas.lean | 2 +- src/Init/Grind/Ring/Envelope.lean | 2 +- src/Lean/Parser/Module.lean | 5 +- src/Lean/Parser/Term/Basic.lean | 7 +- src/Lean/Server/InfoUtils.lean | 6 +- tests/elab/def13.lean | 8 +- tests/elab/grind_11449.lean | 4 +- tests/elab/grind_11539.lean | 4 +- tests/elab/grind_cutsat_tests.lean | 2 +- .../elab/grind_cutsat_tests.lean.out.expected | 2 +- tests/elab/induction1.lean | 20 ++-- tests/elab/matchtac.lean | 46 +++++----- tests/elab/newfrontend1.lean | 64 ++++++------- tests/elab/subst1.lean | 8 +- tests/elab/tactic1.lean | 8 +- tests/elab/task_test2.lean | 18 ++-- tests/elab/typeclass_append.lean | 8 +- tests/elab_bench/simp_congr.lean | 8 +- tests/elab_fail/361.lean.out.expected | 1 - tests/elab_fail/byStrictIndent.lean | 91 +++++++++++++++++-- .../byStrictIndent.lean.out.expected | 54 ++++++++--- .../elab_fail/decreasing_by.lean.out.expected | 1 - tests/elab_fail/hygienicIntro.lean | 48 +++++----- .../elab_fail/hygienicIntro.lean.out.expected | 2 +- .../linterUnusedVariables.lean.out.expected | 1 - tests/elab_fail/namedHoles.lean | 26 +++--- tests/elab_fail/namedHoles.lean.out.expected | 2 +- tests/elab_fail/rewrite.lean | 44 ++++----- tests/elab_fail/rewrite.lean.out.expected | 4 +- tests/server_interactive/plainGoal.lean | 3 +- .../plainGoal.lean.out.expected | 36 ++++---- .../server_interactive/plainGoalEmptyBy.lean | 13 +++ .../plainGoalEmptyBy.lean.out.expected | 12 +++ 33 files changed, 343 insertions(+), 217 deletions(-) create mode 100644 tests/server_interactive/plainGoalEmptyBy.lean create mode 100644 tests/server_interactive/plainGoalEmptyBy.lean.out.expected diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean index 73d12260da..523f0e84f3 100644 --- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean +++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean @@ -1718,7 +1718,7 @@ theorem toArray_roc_append_toArray_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n @[simp] theorem getElem_toArray_roc {m n i : Nat} (_h : i < (m<...=n).toArray.size) : (m<...=n).toArray[i]'_h = m + 1 + i := by -simp [toArray_roc_eq_toArray_rco] + simp [toArray_roc_eq_toArray_rco] theorem getElem?_toArray_roc {m n i : Nat} : (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none := by diff --git a/src/Init/Grind/Ring/Envelope.lean b/src/Init/Grind/Ring/Envelope.lean index 2ad8b2e3fa..d97d60c223 100644 --- a/src/Init/Grind/Ring/Envelope.lean +++ b/src/Init/Grind/Ring/Envelope.lean @@ -193,7 +193,7 @@ theorem mul_assoc (a b c : Q α) : mul (mul a b) c = mul a (mul b c) := by simp [Semiring.left_distrib, Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl theorem mul_one (a : Q α) : mul a (natCast 1) = a := by -obtain ⟨⟨_, _⟩⟩ := a; simp + obtain ⟨⟨_, _⟩⟩ := a; simp theorem one_mul (a : Q α) : mul (natCast 1) a = a := by obtain ⟨⟨_, _⟩⟩ := a; simp diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index 024a5c10df..4986a2e01e 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -127,7 +127,10 @@ private def consumeInput (inputCtx : InputContext) (pmctx : ParserModuleContext) | none => s.pos def topLevelCommandParserFn : ParserFn := - commandParser.fn + -- set position to enforce appropriate indentation of applications etc. + -- We don't do it for nested commands such as in quotations where + -- formatting might be less rigid. + (withPosition commandParser).fn partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (mps : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog := Id.run do let mut pos := mps.pos diff --git a/src/Lean/Parser/Term/Basic.lean b/src/Lean/Parser/Term/Basic.lean index a0d7ffe4ba..f08650b176 100644 --- a/src/Lean/Parser/Term/Basic.lean +++ b/src/Lean/Parser/Term/Basic.lean @@ -84,11 +84,12 @@ Delimiter-free indentation is determined by the *first* tactic of the sequence. tacticSeqBracketed <|> tacticSeq1Indented /-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation. -The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a -position set. -/ +Falls back to an empty tactic sequence when no appropriately indented content follows, producing +an elaboration error (unsolved goals) rather than a parse error. -/ @[builtin_doc, run_builtin_parser_attribute_hooks] def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <| - tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented) + tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented) <|> + node ``tacticSeq1Indented pushNone /- Raw sequence for quotation and grouping -/ @[run_builtin_parser_attribute_hooks] diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index a4b04b2b45..dedfd03304 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -461,8 +461,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String ctxInfo := ctx tacticInfo := ti useAfter := hoverPos > pos && !cs.any (hasNestedTactic pos tailPos) - -- consider every position unindented after an empty `by` to support "hanging" `by` uses - indented := (text.toPosition pos).column > (text.toPosition hoverPos).column && !isEmptyBy ti.stx + indented := (text.toPosition pos).column > (text.toPosition hoverPos).column -- use goals just before cursor as fall-back only -- thus for `(by foo)`, placing the cursor after `foo` shows its state as long -- as there is no state on `)` @@ -485,9 +484,6 @@ where | InfoTree.node (Info.ofMacroExpansionInfo _) cs => cs.any (hasNestedTactic pos tailPos) | _ => false - isEmptyBy (stx : Syntax) : Bool := - -- there are multiple `by` kinds with the same structure - stx.getNumArgs == 2 && stx[0].isToken "by" && stx[1].getNumArgs == 1 && stx[1][0].isMissing partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos.Raw) : Option InfoWithCtx := diff --git a/tests/elab/def13.lean b/tests/elab/def13.lean index f1d185b7b9..5969dbd3ae 100644 --- a/tests/elab/def13.lean +++ b/tests/elab/def13.lean @@ -11,9 +11,9 @@ theorem filter_cons (a : α) (as : List α) : filter p (a :: as) = if p a then a rfl theorem filter_cons_of_pos {a : α} (as : List α) (h : p a) : filter p (a :: as) = a :: filter p as := by -rw [filter_cons]; -rw [if_pos h] + rw [filter_cons]; + rw [if_pos h] theorem filter_cons_of_neg {a : α} (as : List α) (h : ¬ p a) : filter p (a :: as) = filter p as := by -rw [filter_cons]; -rw [if_neg h] + rw [filter_cons]; + rw [if_neg h] diff --git a/tests/elab/grind_11449.lean b/tests/elab/grind_11449.lean index 85a89b6de3..cc100df744 100644 --- a/tests/elab/grind_11449.lean +++ b/tests/elab/grind_11449.lean @@ -36,7 +36,7 @@ example (heq_1 : double n = double j) (heq_2 : Parity.even n ≍ Parity.even j): h_2 n ≍ h_2 j := by -grind + grind opaque q : Nat → Nat → Prop axiom qax : q a b → double a = double b @@ -49,4 +49,4 @@ example (heq_1 : q j n) (heq_2 : Parity.even n ≍ Parity.even j): h_2 n ≍ h_2 j := by -grind + grind diff --git a/tests/elab/grind_11539.lean b/tests/elab/grind_11539.lean index a8a38ad810..955decc54f 100644 --- a/tests/elab/grind_11539.lean +++ b/tests/elab/grind_11539.lean @@ -2,10 +2,10 @@ example {n a b : Nat} (this : (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤ (↑b + (↑a - ↑b)) ^ (n + 1)) : (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n := by -grind (splits := 0) + grind (splits := 0) example {n a b : Nat} (this : (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤ (↑b + (↑a - ↑b)) ^ (n + 1)) : (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n := by -grind + grind diff --git a/tests/elab/grind_cutsat_tests.lean b/tests/elab/grind_cutsat_tests.lean index 812411955d..8fed06496b 100644 --- a/tests/elab/grind_cutsat_tests.lean +++ b/tests/elab/grind_cutsat_tests.lean @@ -8,7 +8,7 @@ example (w x y z : Int) : 3*w - 2*x + y + z = 7 → 4*w + x - y - z = 3 → w = 2 := by -cutsat + cutsat abbrev test1 (a b c d e : Int) := 1337*a + 424242*b - 23*c + 17*d - 101*e ≤ 12345 → diff --git a/tests/elab/grind_cutsat_tests.lean.out.expected b/tests/elab/grind_cutsat_tests.lean.out.expected index 4774642e4b..abe1a18df8 100644 --- a/tests/elab/grind_cutsat_tests.lean.out.expected +++ b/tests/elab/grind_cutsat_tests.lean.out.expected @@ -1,4 +1,4 @@ -grind_cutsat_tests.lean:11:0-11:6: warning: `cutsat` has been deprecated, use `lia` instead +grind_cutsat_tests.lean:11:2-11:8: warning: `cutsat` has been deprecated, use `lia` instead Try this: [apply] lia grind_cutsat_tests.lean:28:0-28:7: warning: declaration uses `sorry` diff --git a/tests/elab/induction1.lean b/tests/elab/induction1.lean index d898cc618f..a5e79d584c 100644 --- a/tests/elab/induction1.lean +++ b/tests/elab/induction1.lean @@ -6,18 +6,18 @@ by { } theorem tst0' {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h -focus - apply Or.inr - assumption -focus - apply Or.inl - assumption + induction h + focus + apply Or.inr + assumption + focus + apply Or.inl + assumption theorem tst1 {p q : Prop } (h : p ∨ q) : q ∨ p := by -induction h with -| inr h2 => exact Or.inl h2 -| inl h1 => exact Or.inr h1 + induction h with + | inr h2 => exact Or.inl h2 + | inl h1 => exact Or.inr h1 theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p := by { diff --git a/tests/elab/matchtac.lean b/tests/elab/matchtac.lean index cc7e899673..2474019d4f 100644 --- a/tests/elab/matchtac.lean +++ b/tests/elab/matchtac.lean @@ -22,33 +22,33 @@ by { } theorem tst4 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p := by -match (generalizing := false) h : xs with -| [] => _ -| z::zs => _ -case match_2 => exact h₁ z zs h -exact h₂ h + match (generalizing := false) h : xs with + | [] => _ + | z::zs => _ + case match_2 => exact h₁ z zs h + exact h₂ h theorem tst5 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:= by -match h with -| Or.inl h => exact Or.inr (Or.inr h) -| Or.inr (Or.inl h) => ?c1 -| Or.inr (Or.inr h) => ?c2 -case c2 => - apply Or.inl - assumption -case c1 => - apply Or.inr - apply Or.inl - assumption + match h with + | Or.inl h => exact Or.inr (Or.inr h) + | Or.inr (Or.inl h) => ?c1 + | Or.inr (Or.inr h) => ?c2 + case c2 => + apply Or.inl + assumption + case c1 => + apply Or.inr + apply Or.inl + assumption theorem tst6 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:= by -match h with -| Or.inl h => exact Or.inr (Or.inr h) -| Or.inr (Or.inl h) => ?c1 -| Or.inr (Or.inr h) => - apply Or.inl - assumption -case c1 => apply Or.inr; apply Or.inl; assumption + match h with + | Or.inl h => exact Or.inr (Or.inr h) + | Or.inr (Or.inl h) => ?c1 + | Or.inr (Or.inr h) => + apply Or.inl + assumption + case c1 => apply Or.inr; apply Or.inl; assumption theorem tst7 {p q r} (h : p ∨ q ∨ r) : r ∨ q ∨ p:= by match h with diff --git a/tests/elab/newfrontend1.lean b/tests/elab/newfrontend1.lean index 287bfc9e08..f889c747b8 100644 --- a/tests/elab/newfrontend1.lean +++ b/tests/elab/newfrontend1.lean @@ -103,32 +103,32 @@ by { } theorem simple8 (x y z : Nat) : y = z → x = x → x = y → x = z := by -intro h1; intro _; intro h3 -refine' Eq.trans ?pre ?post -case post => exact h1 -case pre => exact h3 + intro h1; intro _; intro h3 + refine' Eq.trans ?pre ?post + case post => exact h1 + case pre => exact h3 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z := by -intro h1 _ h3 -trace_state -focus - refine' Eq.trans ?pre ?post - first - | exact h1 - assumption - | exact y - exact h3 - assumption + intro h1 _ h3 + trace_state + focus + refine' Eq.trans ?pre ?post + first + | exact h1 + assumption + | exact y + exact h3 + assumption theorem simple9b (x y z : Nat) : y = z → x = x → x = y → x = z := by -intro h1 _ h3 -trace_state -focus - refine' Eq.trans ?pre ?post - first - | exact h1 - | exact y; exact h3 - assumption + intro h1 _ h3 + trace_state + focus + refine' Eq.trans ?pre ?post + first + | exact h1 + | exact y; exact h3 + assumption theorem simple9c (x y z : Nat) : y = z → x = x → x = y → x = z := by intro h1 _ h3 @@ -187,12 +187,12 @@ by { } theorem simple13 (x y z : Nat) : y = z → x = x → x = y → x = z := by -intro h1 h2 h3 -trace_state -apply @Eq.trans -case b => exact y -trace_state -repeat assumption + intro h1 h2 h3 + trace_state + apply @Eq.trans + case b => exact y + trace_state + repeat assumption theorem simple13b (x y z : Nat) : y = z → x = x → x = y → x = z := by { intro h1 h2 h3; @@ -204,10 +204,10 @@ repeat assumption } theorem simple14 (x y z : Nat) : y = z → x = x → x = y → x = z := by -intros -apply @Eq.trans -case b => exact y -repeat assumption + intros + apply @Eq.trans + case b => exact y + repeat assumption theorem simple15 (x y z : Nat) : y = z → x = x → x = y → x = z := by { diff --git a/tests/elab/subst1.lean b/tests/elab/subst1.lean index d9f1365101..e41118aa3f 100644 --- a/tests/elab/subst1.lean +++ b/tests/elab/subst1.lean @@ -16,9 +16,9 @@ theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z := by def BV (n : Nat) : Type := { a : Array Bool // a.size = n } theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by -subst h1 -apply h2 + subst h1 + apply h2 theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by -subst n -apply h2 + subst n + apply h2 diff --git a/tests/elab/tactic1.lean b/tests/elab/tactic1.lean index 21b08aab47..1542fcb73d 100644 --- a/tests/elab/tactic1.lean +++ b/tests/elab/tactic1.lean @@ -44,10 +44,10 @@ by { } theorem ex7 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by -have : y = z := by apply Eq.symm; assumption -apply Eq.trans -exact h₁ -assumption + have : y = z := by apply Eq.symm; assumption + apply Eq.trans + exact h₁ + assumption theorem ex8 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z := by apply Eq.trans h₁; diff --git a/tests/elab/task_test2.lean b/tests/elab/task_test2.lean index ec619a36dd..78a28b632e 100644 --- a/tests/elab/task_test2.lean +++ b/tests/elab/task_test2.lean @@ -1,17 +1,17 @@ -- def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat := -n.repeat (fun r => - dbg_trace ">> [{i}] {r}"; - xs.foldl (fun a b => a + b) r) -0 + n.repeat (fun r => + dbg_trace ">> [{i}] {r}"; + xs.foldl (fun a b => a + b) r) + 0 def tst (n : Nat) : IO UInt32 := -let ys := (List.replicate n 1); -let ts : List (Task Nat) := (List.range 10).map (fun i => Task.spawn fun _ => run1 (i+1) n ys); -let ns : List Nat := ts.map Task.get; -IO.println (">> " ++ toString ns) *> -pure 0 + let ys := (List.replicate n 1); + let ts : List (Task Nat) := (List.range 10).map (fun i => Task.spawn fun _ => run1 (i+1) n ys); + let ns : List Nat := ts.map Task.get; + IO.println (">> " ++ toString ns) *> + pure 0 /-- info: >> [100, 100, 100, 100, 100, 100, 100, 100, 100, 100] diff --git a/tests/elab/typeclass_append.lean b/tests/elab/typeclass_append.lean index 0cf95002d8..e5390decc6 100644 --- a/tests/elab/typeclass_append.lean +++ b/tests/elab/typeclass_append.lean @@ -17,7 +17,7 @@ instance AppendStep {α : Type} (x : α) (xs₁ xs₂ out : List α) [AppendList {} #synth AppendList -[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] -[200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211] -[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, - 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211] + [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] + [200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211] + [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, + 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211] diff --git a/tests/elab_bench/simp_congr.lean b/tests/elab_bench/simp_congr.lean index f2c6fdd21e..17facca0ae 100644 --- a/tests/elab_bench/simp_congr.lean +++ b/tests/elab_bench/simp_congr.lean @@ -48,14 +48,14 @@ simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] theorem deep_singular_simple (g : L → Unit → L) : deep1(1024, g, iter steps (f b) (iter steps (f a) nil), ()) = deep1(1024, g, iter steps (f a) (iter steps (f b) nil), ()) := by -simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] + simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] axiom g1 : L → Unit → L theorem deep_singular_simple_const : deep1(1024, g1, iter steps (f b) (iter steps (f a) nil), ()) = deep1(1024, g1, iter steps (f a) (iter steps (f b) nil), ()) := by -simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] + simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] -- Provoke regenerating simple congruence theorems unless they are cached or handled otherwise, -- adding `True` with the dependency on `x` here avoids a fast path in simp congruence theorem @@ -64,11 +64,11 @@ simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] theorem deep_singular_prop_dep (g2 : (x : L) → (h : (fun _ => True) x) → L) : deep1(1024, g2, iter steps (f b) (iter steps (f a) nil), True.intro) = deep1(1024, g2, iter steps (f a) (iter steps (f b) nil), True.intro) := by -simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] + simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] axiom g2 : (x : L) → (h : (fun _ => True) x) → L theorem deep_singular_prop_const_dep : deep1(1024, g2, iter steps (f b) (iter steps (f a) nil), True.intro) = deep1(1024, g2, iter steps (f a) (iter steps (f b) nil), True.intro) := by -simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] + simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps] diff --git a/tests/elab_fail/361.lean.out.expected b/tests/elab_fail/361.lean.out.expected index 136be26e5a..bbe924de2b 100644 --- a/tests/elab_fail/361.lean.out.expected +++ b/tests/elab_fail/361.lean.out.expected @@ -1,4 +1,3 @@ -361.lean:1:62-3:7: error: unexpected token 'theorem'; expected '{' or tactic 361.lean:1:60-1:62: error: unsolved goals p q r : Prop h1 : p ∨ q diff --git a/tests/elab_fail/byStrictIndent.lean b/tests/elab_fail/byStrictIndent.lean index fbaeb666de..20e2c6939c 100644 --- a/tests/elab_fail/byStrictIndent.lean +++ b/tests/elab_fail/byStrictIndent.lean @@ -1,15 +1,12 @@ --- +-- Un-indented tactic after top-level `by` parses as empty `by` (unsolved goals) +-- followed by a command parse error for the stray tactic. +theorem byTopLevelBad (n : Nat) (h : n > 1) : n > 1 := by +exact h -- unsolved goals + unexpected identifier --- no indentation on top-level `by` is still allowed -theorem byTopLevelNoIndent (n : Nat) (h : n > 1) : n > 1 := by -exact h - -#print byTopLevelNoIndent - --- +-- Nested `by` without indentation: inner `by` is empty, `sorry` continues in outer scope. theorem byNestedStrictIndent (n : Nat) (h : n > 0) : n > 1 := by have helper : n > 1 := by - sorry -- expected '{' or strict indentation + sorry -- part of outer `by`; inner `by` is empty (unsolved goals) sorry -- @@ -24,3 +21,79 @@ theorem byNestedBad₂ (n : Nat) (h : n > 0) : n > 1 := by sorry sorry -- expected command sorry + +-- When stacking multiple `by` invocations on one line, the indentation of the +-- tactic block is checked against the innermost `withPosition` point (the column +-- of the innermost `have`/`let`/etc.), not against the outermost `by`. +-- So indenting past the outer `by` is not enough if the inner `have` is further right. + +-- Good: each tactic block is indented past its respective `have` +theorem byStackedGood : True := by + have : True := by + exact trivial + exact this + +-- Bad: tactic is indented past the outer `by` (column 0) but not past `have` (column 27) +-- Inner `by` is empty (unsolved goals), stray tactics produce command parse errors. +theorem byStackedBad₁ : True := by have : True := by + exact trivial -- unsolved goals + unexpected identifier + exact this + +-- Bad: same issue with deeper stacking +theorem byStackedBad₂ : True := by have : True := by have : True := by + exact trivial -- unsolved goals + unexpected identifier + exact this + +-- When `by` is inside a command that sets a position (like `#guard_msgs`), +-- `withPosition` at the command level checks against the command's column. +-- The `trivial` at column 2 must be > column of `#guard_msgs` (column 0). +#guard_msgs (drop info) in +example : True := by + trivial + +-- Command-wrapping-command on one line: the proof needs to be indented +-- past the outer command (`#guard_msgs`, col 0), not the inner (`example`). +-- `#guard_msgs in` uses `commandParser` directly, not `topLevelCommandParserFn`, +-- so the inner command does not get its own `withPosition` scope. +#guard_msgs (drop info) in example : True := by + trivial + +-- Same but with the inner command indented +#guard_msgs (drop info) in + example : True := by + trivial + +-- Bad: tactic at column 0 inside #guard_msgs is not indented past the command +#guard_msgs (drop info) in +example : True := by +trivial -- unsolved goals + unexpected identifier + +-- Bad: tactic at column 0 inside inline #guard_msgs +#guard_msgs (drop info) in example : True := by +trivial -- unsolved goals + unexpected identifier + +-- Indented commands inside section: with `withPosition` at command level, +-- the position is saved at the command's column, not at column 0. +-- So proofs must be indented past the command, not just past column 0. +section + theorem indentedGood : True := by + trivial +end + +-- Bad: tactic at column 2 is not indented past `theorem` (column 2) +section + theorem indentedBad : True := by + trivial -- unsolved goals + unexpected identifier +end + +-- Indented non-tactic content: `123` doesn't parse as a tactic, so the +-- empty-by fallback fires (unsolved goals) and `123` is tried as a command. +-- This matches the behavior of non-tactic content on subsequent lines. +theorem fallbackOnNonTactic : True := by + 123 -- unsolved goals + unexpected token + +-- For comparison: non-tactic on second line (after a valid tactic). +-- Same pattern: `123` falls out of the tactic block and gets a command error. +theorem fallbackOnNonTacticSecondLine : True := by + skip + 123 -- unsolved goals + unexpected token diff --git a/tests/elab_fail/byStrictIndent.lean.out.expected b/tests/elab_fail/byStrictIndent.lean.out.expected index 5c57943f85..f2d0cd45ff 100644 --- a/tests/elab_fail/byStrictIndent.lean.out.expected +++ b/tests/elab_fail/byStrictIndent.lean.out.expected @@ -1,24 +1,52 @@ -theorem byTopLevelNoIndent : ∀ (n : Nat), n > 1 → n > 1 := -fun n h => h -byStrictIndent.lean:12:2: error: expected '{' or indented tactic sequence -byStrictIndent.lean:11:25-11:27: error: unsolved goals +byStrictIndent.lean:3:55-3:57: error: unsolved goals +n : Nat +h : n > 1 +⊢ n > 1 +byStrictIndent.lean:4:0-4:5: error: unexpected identifier; expected command +byStrictIndent.lean:8:25-8:27: error: unsolved goals n : Nat h : n > 0 ⊢ n > 1 -byStrictIndent.lean:10:62-11:27: error: unsolved goals +byStrictIndent.lean:10:2-10:7: error: No goals to be solved +byStrictIndent.lean:13:54-15:9: error: unsolved goals n : Nat h : n > 0 helper : n > 1 ⊢ n > 1 -byStrictIndent.lean:16:54-18:9: error: unsolved goals +byStrictIndent.lean:16:3-16:8: error: unexpected token 'sorry'; expected command +byStrictIndent.lean:19:54-21:9: error: unsolved goals n : Nat h : n > 0 helper : n > 1 ⊢ n > 1 -byStrictIndent.lean:19:3-19:8: error: unexpected token 'sorry'; expected command -byStrictIndent.lean:22:54-24:9: error: unsolved goals -n : Nat -h : n > 0 -helper : n > 1 -⊢ n > 1 -byStrictIndent.lean:25:6-25:11: error: unexpected token 'sorry'; expected command +byStrictIndent.lean:22:6-22:11: error: unexpected token 'sorry'; expected command +byStrictIndent.lean:38:50-38:52: error: unsolved goals +⊢ True +byStrictIndent.lean:38:32-38:52: error: unsolved goals +this : True +⊢ True +byStrictIndent.lean:39:2-39:7: error: unexpected identifier; expected command +byStrictIndent.lean:43:68-43:70: error: unsolved goals +⊢ True +byStrictIndent.lean:43:50-43:70: error: unsolved goals +this : True +⊢ True +byStrictIndent.lean:43:32-43:70: error: unsolved goals +this : True +⊢ True +byStrictIndent.lean:44:2-44:7: error: unexpected identifier; expected command +byStrictIndent.lean:68:18-68:20: error: unsolved goals +⊢ True +byStrictIndent.lean:69:0-69:7: error: unexpected identifier; expected command +byStrictIndent.lean:72:45-72:47: error: unsolved goals +⊢ True +byStrictIndent.lean:73:0-73:7: error: unexpected identifier; expected command +byStrictIndent.lean:85:32-85:34: error: unsolved goals +⊢ True +byStrictIndent.lean:86:2-86:9: error: unexpected identifier; expected command +byStrictIndent.lean:92:38-92:40: error: unsolved goals +⊢ True +byStrictIndent.lean:93:2-93:5: error: unexpected token; expected command +byStrictIndent.lean:97:48-98:6: error: unsolved goals +⊢ True +byStrictIndent.lean:99:2-99:5: error: unexpected token; expected command diff --git a/tests/elab_fail/decreasing_by.lean.out.expected b/tests/elab_fail/decreasing_by.lean.out.expected index 474a642aa8..af6287dc37 100644 --- a/tests/elab_fail/decreasing_by.lean.out.expected +++ b/tests/elab_fail/decreasing_by.lean.out.expected @@ -12,7 +12,6 @@ The basic measures relate at each recursive call as follows: 1) 61:29-43 = ? 2) 61:46-62 ? _ Please use `termination_by` to specify a decreasing measure. -decreasing_by.lean:75:13-77:3: error: unexpected token 'end'; expected '{' or tactic decreasing_by.lean:75:0-75:13: error: unsolved goals n m : Nat ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m) diff --git a/tests/elab_fail/hygienicIntro.lean b/tests/elab_fail/hygienicIntro.lean index f3648e2db7..fab06ffef5 100644 --- a/tests/elab_fail/hygienicIntro.lean +++ b/tests/elab_fail/hygienicIntro.lean @@ -2,22 +2,22 @@ set_option tactic.hygienic false in theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by -intro _ h1 h2; -apply h2; -apply h1; -exact a_1 -- Bad practice, using name generated by `intro`. + intro _ h1 h2; + apply h2; + apply h1; + exact a_1 -- Bad practice, using name generated by `intro`. theorem ex2 {a p q r : Prop} : p → (p → q) → (q → r) → r := by -intro _ h1 h2; -apply h2; -apply h1; -exact a_1 -- error "unknown identifier" + intro _ h1 h2; + apply h2; + apply h1; + exact a_1 -- error "unknown identifier" theorem ex3 {a p q r : Prop} : p → (p → q) → (q → r) → r := by -intro _ h1 h2; -apply h2; -apply h1; -assumption + intro _ h1 h2; + apply h2; + apply h1; + assumption example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by cases h₂; @@ -26,25 +26,25 @@ example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by set_option tactic.hygienic false in example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by -cases h₂; -{ apply h₁; exact h }; -- hygiene is disabled -exact h + cases h₂; + { apply h₁; exact h }; -- hygiene is disabled + exact h -- Hygienic versions example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by -cases h₂ with -| inl h => apply h₁; exact h -| inr h => exact h + cases h₂ with + | inl h => apply h₁; exact h + | inr h => exact h example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by -cases h₂; -{ apply h₁; assumption }; -assumption + cases h₂; + { apply h₁; assumption }; + assumption example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by -match h₂ with -| Or.inl _ => apply h₁; assumption -| Or.inr h => exact h + match h₂ with + | Or.inl _ => apply h₁; assumption + | Or.inr h => exact h example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by unhygienic cases h₂ diff --git a/tests/elab_fail/hygienicIntro.lean.out.expected b/tests/elab_fail/hygienicIntro.lean.out.expected index c13c3709e0..b2ba1ac0ba 100644 --- a/tests/elab_fail/hygienicIntro.lean.out.expected +++ b/tests/elab_fail/hygienicIntro.lean.out.expected @@ -1,3 +1,3 @@ -hygienicIntro.lean:14:6-14:9: error(lean.unknownIdentifier): Unknown identifier `a_1` +hygienicIntro.lean:14:8-14:11: error(lean.unknownIdentifier): Unknown identifier `a_1` hygienicIntro.lean:24:20-24:21: error(lean.unknownIdentifier): Unknown identifier `h` hygienicIntro.lean:25:8-25:9: error(lean.unknownIdentifier): Unknown identifier `h` diff --git a/tests/elab_fail/linterUnusedVariables.lean.out.expected b/tests/elab_fail/linterUnusedVariables.lean.out.expected index aa98c51eb2..30e4ce828c 100644 --- a/tests/elab_fail/linterUnusedVariables.lean.out.expected +++ b/tests/elab_fail/linterUnusedVariables.lean.out.expected @@ -85,7 +85,6 @@ a : Nat ⊢ Nat linterUnusedVariables.lean:245:0-245:7: warning: declaration uses `sorry` linterUnusedVariables.lean:246:0-246:7: warning: declaration uses `sorry` -linterUnusedVariables.lean:247:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic linterUnusedVariables.lean:247:27-247:29: error: unsolved goals a : Nat ⊢ Nat diff --git a/tests/elab_fail/namedHoles.lean b/tests/elab_fail/namedHoles.lean index 79269931a7..a480963055 100644 --- a/tests/elab_fail/namedHoles.lean +++ b/tests/elab_fail/namedHoles.lean @@ -11,8 +11,8 @@ x + y #check g ?x ?x -- ok def h1 (x : Nat) : Nat := by -refine g ?hole ?hole; -- it is the same hole -case hole => exact x + refine g ?hole ?hole; -- it is the same hole + case hole => exact x #eval h1 10 @@ -20,8 +20,8 @@ theorem ex1 : h1 10 = 20 := rfl def h2 (x : Nat) : Nat := by -refine g ?hole ?hole; -exact x+x + refine g ?hole ?hole; + exact x+x theorem ex2 : h2 10 = 40 := rfl @@ -35,24 +35,24 @@ def boo (f : Nat → Nat) (g : Bool → Nat) := f (g true) #check boo (fun x => ?hole) (fun y => ?hole) -- error the local contexts of the two holes are incompatible def h3 (x : Nat) : Nat := by -apply boo; -case f => refine fun y => ?hole + 1; exact x; -- `fun y => ?hole + 1` and assigned `?hole := x` -case g => refine fun b => ?hole -- `fun b => ?hole` it works because assignment is compatible + apply boo; + case f => refine fun y => ?hole + 1; exact x; -- `fun y => ?hole + 1` and assigned `?hole := x` + case g => refine fun b => ?hole -- `fun b => ?hole` it works because assignment is compatible #eval h3 10 theorem ex3 : h3 10 = 11 := rfl def h4 (x : Nat) : Nat := by -refine foo (fun y => ?hole + 2) ?hole; --- note that the local context of ?hole has be shrunk by the second occurrence -exact x + refine foo (fun y => ?hole + 2) ?hole; + -- note that the local context of ?hole has be shrunk by the second occurrence + exact x #eval h4 10 theorem ex4 : h4 10 = 12 := rfl def h5 (x : Nat) : Nat := by -apply boo; -case f => intro y; refine ?hole + 1; exact y; -- `fun y => ?hole + 1` and assigned `?hole := y` -case g => refine fun b => ?hole -- error + apply boo; + case f => intro y; refine ?hole + 1; exact y; -- `fun y => ?hole + 1` and assigned `?hole := y` + case g => refine fun b => ?hole -- error diff --git a/tests/elab_fail/namedHoles.lean.out.expected b/tests/elab_fail/namedHoles.lean.out.expected index 408ff990d4..2e763c5043 100644 --- a/tests/elab_fail/namedHoles.lean.out.expected +++ b/tests/elab_fail/namedHoles.lean.out.expected @@ -15,5 +15,5 @@ namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with boo (fun x => ?hole) fun y => sorry : Nat 11 12 -namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context +namedHoles.lean:58:28-58:33: error: synthetic hole has already been defined and assigned to value incompatible with the current context y diff --git a/tests/elab_fail/rewrite.lean b/tests/elab_fail/rewrite.lean index f720e38beb..fb9dba3f80 100644 --- a/tests/elab_fail/rewrite.lean +++ b/tests/elab_fail/rewrite.lean @@ -15,42 +15,42 @@ theorem ex1 {α} (as bs : List α) : as.reverse.reverse ++ [] ++ [] ++ bs ++ bs theorem ex2 {α} (as bs : List α) : as.reverse.reverse ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) := by -rewrite [reverseEq, reverseEq]; -- Error on second reverseEq -done + rewrite [reverseEq, reverseEq]; -- Error on second reverseEq + done axiom zeroAdd (x : Nat) : 0 + x = x theorem ex2a (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by -rewrite [zeroAdd] at h₁ h₂; -trace_state; -subst x; -subst y; -exact rfl + rewrite [zeroAdd] at h₁ h₂; + trace_state; + subst x; + subst y; + exact rfl theorem ex3 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by -rewrite [zeroAdd] at *; -subst x; -subst y; -exact rfl + rewrite [zeroAdd] at *; + subst x; + subst y; + exact rfl theorem ex4 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by -rewrite [appendAssoc] at *; -- Error -done + rewrite [appendAssoc] at *; -- Error + done theorem ex5 (m n k : Nat) (h : 0 + n = m) (h : k = m) : k = n := by -rw [zeroAdd] at *; -trace_state; -- `h` is still a name for `h : k = m` -refine Eq.trans h ?hole; -apply Eq.symm; -assumption + rw [zeroAdd] at *; + trace_state; -- `h` is still a name for `h : k = m` + refine Eq.trans h ?hole; + apply Eq.symm; + assumption theorem ex6 (p q r : Prop) (h₁ : q → r) (h₂ : p ↔ q) (h₃ : p) : r := by -rw [←h₂] at h₁; -exact h₁ h₃ + rw [←h₂] at h₁; + exact h₁ h₃ theorem ex7 (p q r : Prop) (h₁ : q → r) (h₂ : p ↔ q) (h₃ : p) : r := by -rw [h₂] at h₃; -exact h₁ h₃ + rw [h₂] at h₃; + exact h₁ h₃ example (α : Type) (p : Prop) (a b c : α) (h : p → a = b) : a = c := by rw [h _] -- should manifest goal `⊢ p`, like `rw [h]` would diff --git a/tests/elab_fail/rewrite.lean.out.expected b/tests/elab_fail/rewrite.lean.out.expected index a0e129f8e7..87bbe86151 100644 --- a/tests/elab_fail/rewrite.lean.out.expected +++ b/tests/elab_fail/rewrite.lean.out.expected @@ -1,7 +1,7 @@ α : Type u_1 as bs : List α ⊢ as ++ bs ++ bs = as ++ (bs ++ bs) -rewrite.lean:18:20-18:29: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern +rewrite.lean:18:22-18:31: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern (List.reverse ?as).reverse in the target expression as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) @@ -13,7 +13,7 @@ x y z : Nat h₁ : x = y h₂ : y = z ⊢ x = z -rewrite.lean:37:9-37:20: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern in the current goal +rewrite.lean:37:11-37:22: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern in the current goal x y z : Nat h₁ : 0 + x = y diff --git a/tests/server_interactive/plainGoal.lean b/tests/server_interactive/plainGoal.lean index 3ccaad33f0..cbe1d82bf9 100644 --- a/tests/server_interactive/plainGoal.lean +++ b/tests/server_interactive/plainGoal.lean @@ -107,7 +107,7 @@ example : True := by have : True := by -- type here --^ $/lean/plainGoal --- no `this` here either, but seems okay +-- `this` is in scope: empty `by` is parsed successfully --^ $/lean/plainGoal example : True := by @@ -116,7 +116,6 @@ example : True := by --^ $/lean/plainGoal apply this --^ $/lean/plainGoal --- note: no output here at all because of parse error example : False := by -- EOF test diff --git a/tests/server_interactive/plainGoal.lean.out.expected b/tests/server_interactive/plainGoal.lean.out.expected index 599e7a33d0..7d7a00c589 100644 --- a/tests/server_interactive/plainGoal.lean.out.expected +++ b/tests/server_interactive/plainGoal.lean.out.expected @@ -145,64 +145,68 @@ null {"rendered": "no goals", "goals": []} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 107, "character": 4}} -{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} +{"rendered": "```lean\nthis : True\n⊢ True\n```", + "goals": ["this : True\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 109, "character": 2}} -{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} +{"rendered": "```lean\nthis : True\n⊢ True\n```", + "goals": ["this : True\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 114, "character": 4}} -{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} +{"rendered": "```lean\nthis : True\n⊢ True\n```", + "goals": ["this : True\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 116, "character": 2}} -null +{"rendered": "```lean\nthis : True\n⊢ True\n```", + "goals": ["this : True\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 121, "character": 2}} + "position": {"line": 120, "character": 2}} {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 125, "character": 17}} + "position": {"line": 124, "character": 17}} {"rendered": "```lean\np q : Prop\nhp : p\nhq : q\nthis : q ∧ p\n⊢ p ∧ q\n```", "goals": ["p q : Prop\nhp : p\nhq : q\nthis : q ∧ p\n⊢ p ∧ q"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 129, "character": 18}} + "position": {"line": 128, "character": 18}} {"rendered": "```lean\np q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)\n```", "goals": ["p q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 134, "character": 3}} + "position": {"line": 133, "character": 3}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 134, "character": 4}} + "position": {"line": 133, "character": 4}} {"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 140, "character": 34}} + "position": {"line": 139, "character": 34}} {"rendered": "```lean\ncase zero\n⊢ True\n```\n---\n```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```", "goals": ["case zero\n⊢ True", "case succ\nn✝ : Nat\na✝ : True\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 143, "character": 34}} + "position": {"line": 142, "character": 34}} {"rendered": "```lean\ncase zero\n⊢ True\n```\n---\n```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```", "goals": ["case zero\n⊢ True", "case succ\nn✝ : Nat\na✝ : True\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 146, "character": 34}} + "position": {"line": 145, "character": 34}} {"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 154, "character": 2}} + "position": {"line": 153, "character": 2}} {"rendered": "```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n + 0 = 1 + n\n```", "goals": ["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n + 0 = 1 + n"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 154, "character": 3}} + "position": {"line": 153, "character": 3}} {"rendered": "```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1\n```", "goals": ["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 154, "character": 41}} + "position": {"line": 153, "character": 41}} {"rendered": "```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1\n```", "goals": ["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, - "position": {"line": 154, "character": 43}} + "position": {"line": 153, "character": 43}} {"rendered": "no goals", "goals": []} diff --git a/tests/server_interactive/plainGoalEmptyBy.lean b/tests/server_interactive/plainGoalEmptyBy.lean new file mode 100644 index 0000000000..0e28150c30 --- /dev/null +++ b/tests/server_interactive/plainGoalEmptyBy.lean @@ -0,0 +1,13 @@ +-- Test: `by` where `pushNone` fallback fires (non-indented sorry follows) +example : True := by + --^ $/lean/plainGoal + -- hovering with indent +--^ $/lean/plainGoal +-- hovering without +--⬑ $/lean/plainGoal +sorry + +-- Test: "hanging by" at EOF — hover below `by` at column 0 should still show goals +example : True := by +-- type here +--⬑ $/lean/plainGoal diff --git a/tests/server_interactive/plainGoalEmptyBy.lean.out.expected b/tests/server_interactive/plainGoalEmptyBy.lean.out.expected new file mode 100644 index 0000000000..80d96587b4 --- /dev/null +++ b/tests/server_interactive/plainGoalEmptyBy.lean.out.expected @@ -0,0 +1,12 @@ +{"textDocument": {"uri": "file:///plainGoalEmptyBy.lean"}, + "position": {"line": 1, "character": 18}} +{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} +{"textDocument": {"uri": "file:///plainGoalEmptyBy.lean"}, + "position": {"line": 3, "character": 2}} +{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} +{"textDocument": {"uri": "file:///plainGoalEmptyBy.lean"}, + "position": {"line": 5, "character": 0}} +{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]} +{"textDocument": {"uri": "file:///plainGoalEmptyBy.lean"}, + "position": {"line": 11, "character": 0}} +{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}