fix: enforce linebreak between calc steps

src/Init/NotationExtra.lean

@@ -92,7 +92,7 @@ end
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
 syntax calcStep := ppIndent(colGe term " := " term)
-syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine calcStep)*)
+syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine linebreak calcStep)*)
 
 /-- Step-wise reasoning over transitive relations.
 ```

src/Lean/Elab/Calc.lean

@@ -77,7 +77,9 @@ def getCalcFirstStep (step0 : TSyntax ``calcFirstStep) : TermElabM (TSyntax ``ca
 
 def getCalcSteps (steps : TSyntax ``calcSteps) : TermElabM (Array (TSyntax ``calcStep)) :=
   match steps with
-  | `(calcSteps| $step0:calcFirstStep $rest*) => do
+  | `(calcSteps|
+        $step0:calcFirstStep
+        $rest*) => do
     let step0 ← getCalcFirstStep step0
     pure (#[step0] ++ rest)
   | _ => unreachable!

tests/lean/calcErrors.lean

@@ -1,23 +1,37 @@
+/-! # Check basic `calc` error messages and positions -/
+
+/-! Basic proof failure -/
+
 theorem ex1 (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a + b = 0 + c + b :=
   calc  a + b  = b + b     := by rw [h₁]
         _      = 0 + c + b := rfl
 
+/-! Step term mismatch -/
+
 theorem ex2 (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a + b = 0 + c + b :=
   calc  a + b     = b + b     := by rw [h₁]
         0 + c + b = 0 + c + b := rfl
 
+-- fixed
 theorem ex3 (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a + b = 0 + c + b :=
   calc  a + b  = b + b     := by rw [h₁]
         _      = 0 + b + b := by rw [Nat.zero_add]
         _      = 0 + c + b := by rw [h₂]
 
+/-! Initial term mismatch -/
+
 theorem ex4 (p : Nat → Prop) (a b : Nat) (h₁ : p a) (h₂ : p b) : p c :=
   calc  p a := h₁
         _   := h₂
 
+/-! Final term mismatch -/
+
 theorem ex5 (p : Nat → Nat → Prop) (a b : Nat) (h₁ : p a b) (h₂ : p b c) : p a c :=
   calc  p a b := h₁
         p _ c := h₂
+
+/-! Relation with bad signature -/
+
 infix:50 " ≅ "  => HEq
 instance {α β γ} : Trans (· ≅ · : α → β → Prop) (· ≅ · : β → γ → Prop) (· ≅ · : α → γ → Prop) where
   trans h₁ h₂ := HEq.trans h₁ h₂
@@ -26,6 +40,7 @@ theorem ex6 {a : α} {b : β} {c : γ} (h₁ : HEq a b) (h₂ : b ≅ c) : a ≅
   calc a ≅ b := h₁
        _ ≅ c := h₂  -- Error because the last two arguments of HEq are not explicit
 
+-- fixed
 abbrev HEqRel {α β} (a : α) (b : β) := HEq a b
 
 infix:50 "===" => HEqRel
@@ -36,3 +51,11 @@ instance {α β γ} : Trans (HEqRel : α → β → Prop) (HEqRel : β → γ 
 theorem ex7 {a : α} {b : β} {c : γ} (h₁ : a ≅ b) (h₂ : b ≅ c) : a === c :=
   calc a === b := h₁
        _ === c := h₂
+
+/-!
+  By enforcing separating newlines in the `calc` parser, we make sure that the next error reported is at `[`
+  instead of it being interpreted as the beginning of an incomplete calc step. -/
+
+example : 1 + 1 = 2 := by
+  calc 1 + 1 = 1 + 1 := by rfl
+  _ = 2 := by rfl [h]

tests/lean/calcErrors.lean.expected.out

@@ -1,18 +1,19 @@
-calcErrors.lean:3:30-3:33: error: type mismatch
+calcErrors.lean:7:30-7:33: error: type mismatch
   rfl
 has type
   b + b = b + b : Prop
 but is expected to have type
   b + b = 0 + c + b : Prop
-calcErrors.lean:7:8-7:29: error: invalid 'calc' step, left-hand-side is
+calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand-side is
   0 + c + b : Nat
 previous right-hand-side is
   b + b : Nat
-calcErrors.lean:15:8-15:11: error: invalid 'calc' step, relation expected
+calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
   p a
-calcErrors.lean:20:8-20:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
+calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
-calcErrors.lean:27:7-27:12: error: invalid 'calc' step, left-hand-side is
+calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
   γ : Sort u_1
 previous right-hand-side is
   b : β
+calcErrors.lean:61:18-61:19: error: unexpected token '['; expected command