Goals of tactics often lose line breaks

[caochenrui]

Hi. I enabled the "allTactics" option to get goals of tactics, and I found that most line breaks ('\n') were missing, with only a few correctly containing "\n".

First I run lake exe repl. My input to REPL is:

{"cmd" :"import Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\ntheorem lean_workbook_plus_12679 (f : ℝ → ℝ) (h : ∀ x y z : ℝ, (x + y + z) * f (x * y * z) = 0) : f 0 = 0  := by\n  have h₁ := h 0 0 0\n  simp at h₁\n  have h₂ := h 1 0 0\n  simp at h₂\n  have h₃ := h 0 1 0\n  simp at h₃\n  have h₄ := h 0 0 1\n", "allTactics": true}

And its response is:

{"tactics":
 [{"tactic": "have h₁ := h 0 0 0",
   "proofState": 0,
   "pos": {"line": 9, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 ⊢ f 0 = 0",
   "endPos": {"line": 9, "column": 20}},
  {"tactic": "simp at h₁",
   "proofState": 1,
   "pos": {"line": 10, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : (0 + 0 + 0) * f (0 * 0 * 0) = 0 ⊢ f 0 = 0",
   "endPos": {"line": 10, "column": 12}},
  {"tactic": "have h₂ := h 1 0 0",
   "proofState": 2,
   "pos": {"line": 11, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True ⊢ f 0 = 0",
   "endPos": {"line": 11, "column": 20}},
  {"tactic": "simp at h₂",
   "proofState": 3,
   "pos": {"line": 12, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True h₂ : (1 + 0 + 0) * f (1 * 0 * 0) = 0 ⊢ f 0 = 0",
   "endPos": {"line": 12, "column": 12}},
  {"tactic": "have h₃ := h 0 1 0",
   "proofState": 4,
   "pos": {"line": 13, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True h₂ : f 0 = 0 ⊢ f 0 = 0",
   "endPos": {"line": 13, "column": 20}},
  {"tactic": "simp at h₃",
   "proofState": 5,
   "pos": {"line": 14, "column": 2},
   "goals":
   "f : ℝ → ℝ\nh : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0\nh₁ : True\nh₂ : f 0 = 0\nh₃ : (0 + 1 + 0) * f (0 * 1 * 0) = 0\n⊢ f 0 = 0",
   "endPos": {"line": 14, "column": 12}},
  {"tactic": "have h₄ := h 0 0 1",
   "proofState": 6,
   "pos": {"line": 15, "column": 2},
   "goals":
   "f : ℝ → ℝ h : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0 h₁ : True h₂ h₃ : f 0 = 0 ⊢ f 0 = 0",
   "endPos": {"line": 15, "column": 20}}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 8, "column": 110},
   "endPos": {"line": 15, "column": 20},
   "data":
   "unsolved goals\nf : ℝ → ℝ\nh : ∀ (x y z : ℝ), (x + y + z) * f (x * y * z) = 0\nh₁ : True\nh₂ h₃ : f 0 = 0\nh₄ : (0 + 0 + 1) * f (0 * 0 * 1) = 0\n⊢ f 0 = 0"}],
 "env": 0}

So only proofState 5 printed '\n' correctly. Could you please fix this problem?

Version of REPL is adbbfcb, and I tried on v4.9.0-rc1, too.
Version of lean-toolchain is v4.11.0, and I tried on v4.9.0-rc1, too.
Verison of lake is 5.0.0-ec3042d