From 020da5bffbd2bd83498a6c9279e20fb97e0773d7 Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Thu, 29 May 2025 18:10:27 -0400
Subject: [PATCH] fix: behavior of hard line breaks in `Format` strings (#8457)

This PR fixes an issue when including a hard line break in a `Format`
that caused subsequent (ordinary) line breaks to be erroneously
flattened to spaces.

This issue is especially important for displaying notes and hints in
error messages, as these components could appear garbled due to improper
line-break rendering.
---
 src/Init/Data/Format/Basic.lean               |  49 +++++---
 tests/lean/1079.lean.expected.out             |   5 +-
 tests/lean/973b.lean.expected.out             |   3 +-
 tests/lean/discrTreeIota.lean.expected.out    |   5 +-
 tests/lean/exceptionalTrace.lean.expected.out |   3 +-
 tests/lean/run/1234.lean                      |  15 ++-
 tests/lean/run/1380.lean                      |   5 +-
 tests/lean/run/1815.lean                      |   5 +-
 tests/lean/run/3257.lean                      |   5 +-
 tests/lean/run/790.lean                       |   5 +-
 tests/lean/run/binderNameHintSimp.lean        |   5 +-
 tests/lean/run/docstringRewrites.lean         |   8 +-
 tests/lean/run/fixedParams.lean               |  10 +-
 tests/lean/run/formatHardLineBreaks.lean      | 105 ++++++++++++++++++
 tests/lean/run/grind_pre.lean                 |   6 +-
 tests/lean/run/info_trees.lean                |  47 ++++----
 tests/lean/run/trace.lean                     |   3 +-
 tests/lean/simp_trace.lean.expected.out       |  80 ++++++++++---
 tests/lean/test_extern.lean.expected.out      |   5 +-
 19 files changed, 297 insertions(+), 72 deletions(-)
 create mode 100644 tests/lean/run/formatHardLineBreaks.lean

diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean
index c2c981c16f..2a9afcc719 100644
--- a/src/Init/Data/Format/Basic.lean
+++ b/src/Init/Data/Format/Basic.lean
@@ -142,17 +142,36 @@ private structure WorkItem where
   indent : Int
   activeTags : Nat
 
+/--
+A directive indicating whether a given work group is able to be flattened.
+
+- `allow` indicates that the group is allowed to be flattened; its argument is `true` if
+  there is sufficient space for it to be flattened (and so it should be), or `false` if not.
+- `disallow` means that this group should not be flattened irrespective of space concerns.
+  This is used at levels of a `Format` outside of any flattening groups. It is necessary to track
+  this so that, after a hard line break, we know whether to try to flatten the next line.
+-/
+inductive FlattenAllowability where
+  | allow (fits : Bool)
+  | disallow
+  deriving BEq
+
+/-- Whether the given directive indicates that flattening should occur. -/
+def FlattenAllowability.shouldFlatten : FlattenAllowability → Bool
+  | allow true => true
+  | _ => false
+
 private structure WorkGroup where
-  flatten : Bool
-  flb     : FlattenBehavior
-  items   : List WorkItem
+  fla   : FlattenAllowability
+  flb   : FlattenBehavior
+  items : List WorkItem
 
 private partial def spaceUptoLine' : List WorkGroup → Nat → Nat → SpaceResult
   |   [],                         _,   _ => {}
   |   { items := [],    .. }::gs, col, w => spaceUptoLine' gs col w
   | g@{ items := i::is, .. }::gs, col, w =>
     merge w
-      (spaceUptoLine i.f g.flatten (w + col - i.indent) w)
+      (spaceUptoLine i.f g.fla.shouldFlatten (w + col - i.indent) w)
       (spaceUptoLine' ({ g with items := is }::gs) col)
 
 /-- A monad in which we can pretty-print `Format` objects. -/
@@ -169,11 +188,11 @@ open MonadPrettyFormat
 private def pushGroup (flb : FlattenBehavior) (items : List WorkItem) (gs : List WorkGroup) (w : Nat) [Monad m] [MonadPrettyFormat m] : m (List WorkGroup) := do
   let k  ← currColumn
   -- Flatten group if it + the remainder (gs) fits in the remaining space. For `fill`, measure only up to the next (ungrouped) line break.
-  let g  := { flatten := flb == FlattenBehavior.allOrNone, flb := flb, items := items : WorkGroup }
+  let g  := { fla := .allow (flb == FlattenBehavior.allOrNone), flb := flb, items := items : WorkGroup }
   let r  := spaceUptoLine' [g] k (w-k)
   let r' := merge (w-k) r (spaceUptoLine' gs k)
   -- Prevent flattening if any item contains a hard line break, except within `fill` if it is ungrouped (=> unflattened)
-  return { g with flatten := !r.foundFlattenedHardLine && r'.space <= w-k }::gs
+  return { g with fla := .allow (!r.foundFlattenedHardLine && r'.space <= w-k) }::gs
 
 private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGroup → m Unit
   | []                           => pure ()
@@ -200,11 +219,15 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         pushNewline i.indent.toNat
         let is := { i with f := text (s.extract (s.next p) s.endPos) }::is
         -- after a hard line break, re-evaluate whether to flatten the remaining group
-        pushGroup g.flb is gs w >>= be w
+        -- note that we shouldn't start flattening after a hard break outside a group
+        if g.fla == .disallow then
+          be w (gs' is)
+        else
+          pushGroup g.flb is gs w >>= be w
     | line =>
       match g.flb with
       | FlattenBehavior.allOrNone =>
-        if g.flatten then
+        if g.fla.shouldFlatten then
           -- flatten line = text " "
           pushOutput " "
           endTags i.activeTags
@@ -220,10 +243,10 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           endTags i.activeTags
           pushGroup FlattenBehavior.fill is gs w >>= be w
         -- if preceding fill item fit in a single line, try to fit next one too
-        if g.flatten then
+        if g.fla.shouldFlatten then
           let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length)
             | panic "unreachable"
-          if g'.flatten then
+          if g'.fla.shouldFlatten then
             pushOutput " "
             endTags i.activeTags
             be w gs'  -- TODO: use `return`
@@ -232,7 +255,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         else
           breakHere
     | align force =>
-      if g.flatten && !force then
+      if g.fla.shouldFlatten && !force then
         -- flatten (align false) = nil
         endTags i.activeTags
         be w (gs' is)
@@ -247,7 +270,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           endTags i.activeTags
           be w (gs' is)
     | group f flb =>
-      if g.flatten then
+      if g.fla.shouldFlatten then
         -- flatten (group f) = flatten f
         be w (gs' ({ i with f }::is))
       else
@@ -256,7 +279,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
 /-- Render the given `f : Format` with a line width of `w`.
 `indent` is the starting amount to indent each line by. -/
 def prettyM (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [MonadPrettyFormat m] : m Unit :=
-  be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent, activeTags := 0 }]}]
+  be w [{ flb := FlattenBehavior.allOrNone, fla := .disallow, items := [{ f := f, indent, activeTags := 0 }]}]
 
 /-- Create a format `l ++ f ++ r` with a flatten group.
 FlattenBehaviour is `allOrNone`; for `fill` use `bracketFill`. -/
diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out
index f90c4de209..a715447b14 100644
--- a/tests/lean/1079.lean.expected.out
+++ b/tests/lean/1079.lean.expected.out
@@ -11,4 +11,7 @@
       ?a = ?a
     with
       Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.rewrite] imp_self:10000: False → False ==> True
+[Meta.Tactic.simp.rewrite] imp_self:10000:
+      False → False
+    ==>
+      True
diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out
index 249335fe41..573180ab90 100644
--- a/tests/lean/973b.lean.expected.out
+++ b/tests/lean/973b.lean.expected.out
@@ -1,5 +1,6 @@
 973b.lean:5:8-5:10: warning: declaration uses 'sorry'
 [Meta.Tactic.simp.discharge] ex discharge ❌️
       ?p x
-[Meta.Tactic.simp.discharge] ex discharge ❌️ ?p (f x)
+[Meta.Tactic.simp.discharge] ex discharge ❌️
+      ?p (f x)
 973b.lean:9:8-9:11: warning: declaration uses 'sorry'
diff --git a/tests/lean/discrTreeIota.lean.expected.out b/tests/lean/discrTreeIota.lean.expected.out
index f769cff125..f7247adcd5 100644
--- a/tests/lean/discrTreeIota.lean.expected.out
+++ b/tests/lean/discrTreeIota.lean.expected.out
@@ -2,4 +2,7 @@
       default
     ==>
       PUnit.unit
-[Meta.Tactic.simp.rewrite] eq_self:1000: PUnit.unit = x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      PUnit.unit = x
+    ==>
+      True
diff --git a/tests/lean/exceptionalTrace.lean.expected.out b/tests/lean/exceptionalTrace.lean.expected.out
index 5e9622086b..df628a5c5c 100644
--- a/tests/lean/exceptionalTrace.lean.expected.out
+++ b/tests/lean/exceptionalTrace.lean.expected.out
@@ -5,4 +5,5 @@ use `set_option diagnostics true` to get diagnostic information
     rt + 1
   [Elab.step] expected type: <not-available>, term
       binop% HAdd.hAdd✝ rt 1
-    [Elab.step] expected type: <not-available>, term rt
+    [Elab.step] expected type: <not-available>, term
+        rt
diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean
index 59c63f092b..b4bd842987 100644
--- a/tests/lean/run/1234.lean
+++ b/tests/lean/run/1234.lean
@@ -28,7 +28,10 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
       if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩
     ==>
       ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] eq_self:1000: ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      ⟨v, ⋯⟩ = ⟨v, ⋯⟩
+    ==>
+      True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -65,7 +68,10 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
       if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩
     ==>
       ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] eq_self:1000: ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      ⟨v, ⋯⟩ = ⟨v, ⋯⟩
+    ==>
+      True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -100,7 +106,10 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
       if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩
     ==>
       ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] eq_self:1000: ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      ⟨v, ⋯⟩ = ⟨v, ⋯⟩
+    ==>
+      True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean
index d3896189d4..6858b17d54 100644
--- a/tests/lean/run/1380.lean
+++ b/tests/lean/run/1380.lean
@@ -21,7 +21,10 @@ trace: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
         v₁ < v₂
       ==>
         True
-[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000: v₂ = v₁ ==> False
+[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000:
+      v₂ = v₁
+    ==>
+      False
 -/
 #guard_msgs in
 set_option trace.Meta.Tactic.simp true in
diff --git a/tests/lean/run/1815.lean b/tests/lean/run/1815.lean
index 3b33f5ed8f..8cb4563e0b 100644
--- a/tests/lean/run/1815.lean
+++ b/tests/lean/run/1815.lean
@@ -13,7 +13,10 @@ trace: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> d
     ==>
       a * default
 [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected a * default ==> default * a
-[Meta.Tactic.simp.rewrite] eq_self:1000: Left a = a * default ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      Left a = a * default
+    ==>
+      True
 -/
 #guard_msgs in
 example (a : α) : Left a = Right a := by
diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean
index 329c452aee..8a448d4518 100644
--- a/tests/lean/run/3257.lean
+++ b/tests/lean/run/3257.lean
@@ -20,7 +20,10 @@ trace: [Meta.Tactic.simp.discharge] bar discharge ✅️
         T
       ==>
         True
-[Meta.Tactic.simp.rewrite] bar:1000: U ==> True
+[Meta.Tactic.simp.rewrite] bar:1000:
+      U
+    ==>
+      True
 -/
 #guard_msgs in
 example : U := by
diff --git a/tests/lean/run/790.lean b/tests/lean/run/790.lean
index e0d88bbe31..368b1084d3 100644
--- a/tests/lean/run/790.lean
+++ b/tests/lean/run/790.lean
@@ -20,7 +20,10 @@ trace: [Meta.Tactic.simp.rewrite] differential_of_linear:1000:
       differential f x dx
     ==>
       f dx
-[Meta.Tactic.simp.rewrite] eq_self:1000: f dx = f dx ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      f dx = f dx
+    ==>
+      True
 -/
 #guard_msgs in
 example {Y : Type} [Vec Y] (f : Nat → Y) (x dx : Nat)
diff --git a/tests/lean/run/binderNameHintSimp.lean b/tests/lean/run/binderNameHintSimp.lean
index 5aaa13178e..da75cc21b4 100644
--- a/tests/lean/run/binderNameHintSimp.lean
+++ b/tests/lean/run/binderNameHintSimp.lean
@@ -17,7 +17,10 @@ trace: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
     ==>
       z
 [Meta.Tactic.simp.rewrite] unfold z, z ==> 0
-[Meta.Tactic.simp.rewrite] eq_self:1000: 0 = 0 ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      0 = 0
+    ==>
+      True
 -/
 #guard_msgs in
 example : binderNameHint x y z = 0 := by
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index 43ef416a3b..9f4bdc9e89 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -107,7 +107,9 @@ info: Errors: ⏎
     Missing documentation type
    • "lean-manual://f":
     Unknown documentation type 'f'. Expected 'section'.
-   • "lean-manual://a/": Unknown documentation type 'a'. Expected 'section'.  ⏎
+   • "lean-manual://a/":
+    Unknown documentation type 'a'. Expected 'section'.
+
 ---
 info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b"
 -/
@@ -120,7 +122,9 @@ info: Errors: ⏎
     Missing documentation type
    • "lean-manual://f":
     Unknown documentation type 'f'. Expected 'section'.
-   • "lean-manual://a/b": Unknown documentation type 'a'. Expected 'section'.  ⏎
+   • "lean-manual://a/b":
+    Unknown documentation type 'a'. Expected 'section'.
+
 ---
 info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b "
 -/
diff --git a/tests/lean/run/fixedParams.lean b/tests/lean/run/fixedParams.lean
index d857e616ae..e16a5d4c6c 100644
--- a/tests/lean/run/fixedParams.lean
+++ b/tests/lean/run/fixedParams.lean
@@ -59,7 +59,9 @@ namespace Ex4
 trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3:
     In foo c n b m
     m not matched
-[Elab.definition.fixedParams] getFixedParams: • [#1 #3] ❌ [#3 #1] ❌ • [#3 #1] ❌ [#1 #3] ❌
+[Elab.definition.fixedParams] getFixedParams:
+      • [#1 #3] ❌ [#3 #1] ❌
+      • [#3 #1] ❌ [#1 #3] ❌
 -/
 #guard_msgs in
 mutual
@@ -79,7 +81,8 @@ trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
 [Elab.definition.fixedParams] getFixedParams: notFixed 0 2:
     In app as bs
     x✝ =/= bs
-[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ ❌
+[Elab.definition.fixedParams] getFixedParams:
+      • [#1] ❌ ❌
 -/
 #guard_msgs(trace) in
 def app : List α → List α → List α
@@ -90,7 +93,8 @@ def app : List α → List α → List α
 trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
     In app' as bs
     as✝ =/= as
-[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ [#3]
+[Elab.definition.fixedParams] getFixedParams:
+      • [#1] ❌ [#3]
 -/
 #guard_msgs(trace) in
 def app' (as : List α) (bs : List α) : List α :=
diff --git a/tests/lean/run/formatHardLineBreaks.lean b/tests/lean/run/formatHardLineBreaks.lean
new file mode 100644
index 0000000000..3508801770
--- /dev/null
+++ b/tests/lean/run/formatHardLineBreaks.lean
@@ -0,0 +1,105 @@
+import Lean.Data.Format
+import Lean.Meta.Basic
+
+/-! # Hard line breaks in `Format` text
+
+Hard line breaks in `Format`s should not induce inescapable flattening groups, which they did in
+previous versions of Lean.
+-/
+
+open Lean Meta
+
+/--
+info: A
+B
+C
+-/
+#guard_msgs (whitespace := exact) in
+#eval
+  let f : Format := .text "A\nB" ++ .line ++ "C"
+  IO.println f.pretty
+
+/--
+info: A
+  B
+C
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do
+  logInfo <| m!"A{indentD "B"}" ++ Format.line ++ "C"
+
+/--
+info: A
+B
+  C
+D
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do
+  let text := toMessageData
+  let line := toMessageData Format.line
+  logInfo <| text m!"A" ++ line ++ .nest 2 (m!"B" ++ line ++ m!"C") ++ line ++ "D"
+
+/--
+info: a
+b
+a b
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do logInfo (m!"a" ++ Format.line ++ m!"b" ++ Format.line ++ .group m!"a\nb")
+
+/--
+info: Indented expression:
+  Nat
+Bulleted list:
+  • A
+  • B
+---
+info: Indented expression:
+  Nat
+Bulleted list:
+  • A
+  • B
+---
+info: Bulleted list:
+  • A
+  • B
+Indented expression:
+  Nat
+---
+info: Bulleted list:
+  • A
+  • B
+Indented expression:
+  Nat
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do
+  let e := m!"Indented expression:{indentExpr (.const `Nat [])}"
+  let l := m!"Bulleted list:{indentD m!"• A\n• B"}"
+  logInfo (e ++ .ofFormat (.text "\n") ++ l)
+  logInfo (e ++ Format.line ++ l)
+  logInfo (l ++ .ofFormat (.text "\n") ++ e)
+  logInfo (l ++ Format.line ++ e)
+
+-- *Within* flattening groups, flattening should be recomputed after a hard line break:
+/--
+info: A
+A long line
+B
+C
+D
+
+A
+A long line
+B C
+D
+-/
+#guard_msgs (whitespace := exact) in
+#eval
+  let f : Format := .text "A" ++ .line ++ .group ("A long line" ++ .line ++ .text "B" ++ .line ++ "C") ++ .line ++ "D"
+  let f' : Format := .text "A" ++ .line ++ .group ("A long line\nB" ++ .line ++ "C") ++ .line ++ "D"
+  do
+  IO.println (f.pretty 10)
+  IO.println ""
+  IO.println (f'.pretty 10)
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 0e97608e90..50b8b7b049 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -208,7 +208,11 @@ h_2 : ¬f a = g b
     [eqc] {a, b}
     [eqc] {f, g}
 [grind] Issues
-  [issue] found congruence between g b and f a but functions have different types
+  [issue] found congruence between
+        g b
+      and
+        f a
+      but functions have different types
 -/
 #guard_msgs (error) in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean
index 47710d5aa4..0429c1c26a 100644
--- a/tests/lean/run/info_trees.lean
+++ b/tests/lean/run/info_trees.lean
@@ -3,58 +3,58 @@
 -- it is fine to simply remove the `#guard_msgs` and expected output.
 
 /--
-info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
-  • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩ @ Lean.Elab.Term.elabIdent
-    • [.] Nat : some Sort.{?_uniq.1} @ ⟨82, 15⟩-⟨82, 18⟩
-    • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩
-  • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩
-  • 0 ≤ n : Prop @ ⟨82, 22⟩-⟨82, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
+info: • command @ ⟨83, 0⟩-⟨83, 40⟩ @ Lean.Elab.Command.elabDeclaration
+  • Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩ @ Lean.Elab.Term.elabIdent
+    • [.] Nat : some Sort.{?_uniq.1} @ ⟨83, 15⟩-⟨83, 18⟩
+    • Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩
+  • n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩
+  • 0 ≤ n : Prop @ ⟨83, 22⟩-⟨83, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
     • Macro expansion
       0 ≤ n
       ===>
       binrel% LE.le✝ 0 n
-      • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
-        • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩†
-          • [.] LE.le✝ : none @ ⟨82, 22⟩†-⟨82, 27⟩†
-          • 0 : Nat @ ⟨82, 22⟩-⟨82, 23⟩ @ Lean.Elab.Term.elabNumLit
-          • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩ @ Lean.Elab.Term.elabIdent
-            • [.] n : none @ ⟨82, 26⟩-⟨82, 27⟩
-            • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩
+      • 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
+        • 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩†
+          • [.] LE.le✝ : none @ ⟨83, 22⟩†-⟨83, 27⟩†
+          • 0 : Nat @ ⟨83, 22⟩-⟨83, 23⟩ @ Lean.Elab.Term.elabNumLit
+          • n : Nat @ ⟨83, 26⟩-⟨83, 27⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : none @ ⟨83, 26⟩-⟨83, 27⟩
+            • n : Nat @ ⟨83, 26⟩-⟨83, 27⟩
   • CustomInfo(Lean.Elab.Term.AsyncBodyInfo)
-    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩
-    • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩
+    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩
+    • n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩
     • CustomInfo(Lean.Elab.Term.BodyInfo)
-      • Tactic @ ⟨82, 31⟩-⟨82, 40⟩
+      • Tactic @ ⟨83, 31⟩-⟨83, 40⟩
         (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
         before ⏎
         n : Nat
         ⊢ 0 ≤ n
         after no goals
-        • Tactic @ ⟨82, 31⟩-⟨82, 33⟩
+        • Tactic @ ⟨83, 31⟩-⟨83, 33⟩
           "by"
           before ⏎
           n : Nat
           ⊢ 0 ≤ n
           after no goals
-          • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
+          • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
             (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
             before ⏎
             n : Nat
             ⊢ 0 ≤ n
             after no goals
-            • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
+            • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
               (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
               before ⏎
               n : Nat
               ⊢ 0 ≤ n
               after no goals
-              • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
+              • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
                 (Tactic.exact? "exact?" [])
                 before ⏎
                 n : Nat
                 ⊢ 0 ≤ n
                 after no goals
-                • Tactic @ ⟨82, 34⟩†-⟨82, 40⟩† @ Lean.Elab.Tactic.evalExact
+                • Tactic @ ⟨83, 34⟩†-⟨83, 40⟩† @ Lean.Elab.Tactic.evalExact
                   (Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
                   before ⏎
                   n : Nat
@@ -71,9 +71,10 @@ info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
                   {"suggestions": [{"suggestion": "exact Nat.zero_le n"}],
                    "style": null,
                    "range":
-                   {"start": {"line": 81, "character": 34}, "end": {"line": 81, "character": 40}},
+                   {"start": {"line": 82, "character": 34}, "end": {"line": 82, "character": 40}},
                    "isInline": true,
-                   "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩
+                   "header": "Try this: "}
+    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩
 ---
 info: Try this: exact Nat.zero_le n
 -/
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index 421eebd47a..77d8d9a3ef 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -73,7 +73,8 @@ info: [module] message
   [module] hello
                world
   [bughunt] at test2
-  [module] hello world
+  [module] hello
+               world
 [module] hello
              world
 [bughunt] at end of tst3
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index d8552c4d0d..8070fab5c7 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -1,10 +1,16 @@
 Try this: simp only [f, reduceCtorEq]
 [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = []
-[Meta.Tactic.simp.rewrite] eq_self:1000: False = False ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      False = False
+    ==>
+      True
 Try this: simp only [length, gt_iff_lt]
 [Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1
 [Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1
-[Meta.Tactic.simp.rewrite] gt_iff_lt:1000: length as + 1 + 1 > length as ==> length as < length as + 1 + 1
+[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:
+      length as + 1 + 1 > length as
+    ==>
+      length as < length as + 1 + 1
 Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left]
 [Meta.Tactic.simp.rewrite] unfold fact, fact (x + 1) ==> (x + 1) * fact x
 [Meta.Tactic.simp.rewrite] gt_iff_lt:1000:
@@ -15,15 +21,24 @@ Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_l
       0 < x + 1
     ==>
       True
-[Meta.Tactic.simp.rewrite] Nat.mul_pos_iff_of_pos_left:1000: 0 < (x + 1) * fact x ==> 0 < fact x
+[Meta.Tactic.simp.rewrite] Nat.mul_pos_iff_of_pos_left:1000:
+      0 < (x + 1) * fact x
+    ==>
+      0 < fact x
 Try this: simp only [head]
 [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with
     | [] => default
     | a :: tail => a
-[Meta.Tactic.simp.rewrite] eq_self:1000: a = a ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      a = a
+    ==>
+      True
 Try this: simp only [foo]
 [Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10
-[Meta.Tactic.simp.rewrite] eq_self:1000: 10 + x = 10 + x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      10 + x = 10 + x
+    ==>
+      True
 Try this: simp only [g, pure]
 [Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x;
       pure x).run
@@ -43,13 +58,19 @@ Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modify
 [Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s
 [Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s)
 [Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g s) s ==> pure (PUnit.unit, g s)
-[Meta.Tactic.simp.rewrite] eq_self:1000: (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s)
+    ==>
+      True
 Try this: simp only [bla, h]
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] eq_self:1000: x + x = x + x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      x + x = x + x
+    ==>
+      True
 Try this: simp only [h, Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000:
       1 ≤ x
@@ -59,7 +80,10 @@ Try this: simp only [h, Nat.sub_add_cancel]
       x - 1 + 1
     ==>
       x
-[Meta.Tactic.simp.rewrite] eq_self:1000: x + 2 = x + 2 ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      x + 2 = x + 2
+    ==>
+      True
 Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite]
 [Meta.Tactic.simp.rewrite] h:1000:
       1 ≤ x
@@ -77,25 +101,37 @@ Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite
       if _h : 1 ≤ x then x else 0
     ==>
       if 1 ≤ x then x else 0
-[Meta.Tactic.simp.rewrite] eq_self:1000: (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0
+    ==>
+      True
 Try this: simp only [and_self]
 [Meta.Tactic.simp.rewrite] and_self:1000:
       b ∧ b
     ==>
       b
-[Meta.Tactic.simp.rewrite] iff_self:1000: a ∧ b ↔ a ∧ b ==> True
+[Meta.Tactic.simp.rewrite] iff_self:1000:
+      a ∧ b ↔ a ∧ b
+    ==>
+      True
 Try this: simp only [my_thm]
 [Meta.Tactic.simp.rewrite] my_thm:1000:
       b ∧ b
     ==>
       b
-[Meta.Tactic.simp.rewrite] eq_self:1000: (a ∧ b) = (a ∧ b) ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      (a ∧ b) = (a ∧ b)
+    ==>
+      True
 Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000:
       x - 1 + 1
     ==>
       x
-[Meta.Tactic.simp.rewrite] eq_self:1000: x = x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      x = x
+    ==>
+      True
 simp_trace.lean:86:0-86:7: warning: declaration uses 'sorry'
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
@@ -119,7 +155,10 @@ h₂ : xs.length + ys.length = y
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] List.length_append:1000: (xs ++ ys).length ==> xs.length + ys.length
+[Meta.Tactic.simp.rewrite] List.length_append:1000:
+      (xs ++ ys).length
+    ==>
+      xs.length + ys.length
 Try this: simp only [bla, h, List.length_append] at *
 simp_trace.lean:107:101-108:53: error: unsolved goals
 x y : Nat
@@ -132,7 +171,10 @@ h₂ : xs.length + ys.length = y
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] List.length_append:1000: (xs ++ ys).length ==> xs.length + ys.length
+[Meta.Tactic.simp.rewrite] List.length_append:1000:
+      (xs ++ ys).length
+    ==>
+      xs.length + ys.length
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
@@ -162,7 +204,10 @@ Try this: simp only [← my_thm']
       P ∧ P
     ==>
       P
-[Meta.Tactic.simp.rewrite] iff_self:1000: P ↔ P ==> True
+[Meta.Tactic.simp.rewrite] iff_self:1000:
+      P ↔ P
+    ==>
+      True
 Try this: simp only [h]
 [Meta.Tactic.simp.rewrite] h:1000:
       P
@@ -183,4 +228,7 @@ Try this: simp_all only
       n
     ==>
       m
-[Meta.Tactic.simp.rewrite] h₁:1000: n ==> m
+[Meta.Tactic.simp.rewrite] h₁:1000:
+      n
+    ==>
+      m
diff --git a/tests/lean/test_extern.lean.expected.out b/tests/lean/test_extern.lean.expected.out
index 25c3a995a9..64482b2ddf 100644
--- a/tests/lean/test_extern.lean.expected.out
+++ b/tests/lean/test_extern.lean.expected.out
@@ -1,3 +1,6 @@
 test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute
 test_extern.lean:15:0-15:13: error: native implementation did not agree with reference implementation!
-Compare the outputs of: #eval g  and #eval 4
+Compare the outputs of:
+#eval g
+ and
+#eval 4