From f1d3527fe8cc24f4b7cb760bedbe74d021634417 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 8 Oct 2024 10:36:08 -0700
Subject: [PATCH] fix: have `Lean.Meta.ppGoal` use hard newlines (#5640)

This function uses soft newlines in many places where hard newlines are
more appropriate. Pointed out by @gebner in #1967.
---
 src/Lean/Meta/PPGoal.lean              | 4 ++--
 tests/lean/issue2981.lean.expected.out | 3 ++-
 tests/lean/simpDisch.lean.expected.out | 7 ++++++-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 1ca8d65789..10cc6c2f7e 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -33,7 +33,7 @@ register_builtin_option pp.showLetValues : Bool := {
 }
 
 private def addLine (fmt : Format) : Format :=
-  if fmt.isNil then fmt else fmt ++ Format.line
+  if fmt.isNil then fmt else fmt ++ "\n"
 
 def getGoalPrefix (mvarDecl : MetavarDecl) : String :=
   if isLHSGoal? mvarDecl.type |>.isSome then
@@ -99,6 +99,6 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
       let fmt := fmt ++ getGoalPrefix mvarDecl ++ Format.nest indent typeFmt
       match mvarDecl.userName with
       | Name.anonymous => return fmt
-      | name           => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
+      | name           => return "case " ++ format name.eraseMacroScopes ++ "\n" ++ fmt
 
 end Lean.Meta
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
index 6551019d6c..284f10ec71 100644
--- a/tests/lean/issue2981.lean.expected.out
+++ b/tests/lean/issue2981.lean.expected.out
@@ -8,4 +8,5 @@ Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
 ⊢ n < n.succ
-n m : Nat ⊢ n < n.succ
+n m : Nat
+⊢ n < n.succ
diff --git a/tests/lean/simpDisch.lean.expected.out b/tests/lean/simpDisch.lean.expected.out
index c6e58fe6a0..e7b4bfc6e4 100644
--- a/tests/lean/simpDisch.lean.expected.out
+++ b/tests/lean/simpDisch.lean.expected.out
@@ -8,7 +8,12 @@ h1 : x ≠ 0
 h2 : y ≠ 0
 h3 : x = y
 ⊢ x ≠ 0
-case simp.discharger x y : Nat h1 : x ≠ 0 h2 : y ≠ 0 h3 : x = y ⊢ y ≠ 0
+case simp.discharger
+x y : Nat
+h1 : x ≠ 0
+h2 : y ≠ 0
+h3 : x = y
+⊢ y ≠ 0
 x y : Nat
 h1 : x ≠ 0
 h2 : y ≠ 0