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.
2025-05-29 18:10:27 -04:00 · 2025-05-29 18:10:27 -04:00 · 020da5bffb
commit 020da5bffb
parent bc8189b61d
19 changed files with 297 additions and 72 deletions
--- 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`. -/
--- 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
--- 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'
--- 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
--- 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
--- 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):
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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 "
 -/
--- 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 α :=
--- a/tests/lean/run/formatHardLineBreaks.lean
+++ 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)
--- 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
--- 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
 -/
--- 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
--- 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
--- 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