correct whitespace when pretty printing goals

leanprover-community · Nov 28, 2023 · 38365a7 · 38365a7
1 parent 5b7e0d4
commit 38365a7
Show file tree

Hide file tree

Showing 8 changed files with 10 additions and 9 deletions.
diff --git a/README.md b/README.md
@@ -69,7 +69,7 @@ Example usage:
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 29},
-   "goal": "x : Unit ⊢ Nat",
+   "goal": "x : Unit\n⊢ Nat",
    "endPos": {"line": 1, "column": 34}}],
  "messages":
  [{"severity": "warning",

diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -100,7 +100,8 @@ def sorries (trees : List InfoTree) : M m (List Sorry) :=
     fun ⟨ctx, g, pos, endPos⟩ => do
       let (goal, proofState) ← match g with
       | .tactic g => do
-         pure (s!"{(← ctx.ppGoals [g])}".trim, some (← ProofSnapshot.create ctx none [g]))
+         let s ← ProofSnapshot.create ctx none [g]
+         pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
       | .term lctx (some t) => do
          pure (s!"⊢ {← ctx.ppExpr lctx t}", some (← ProofSnapshot.create ctx lctx [] [t]))
       | .term _ none => unreachable!

diff --git a/test.sh b/test.sh
@@ -22,7 +22,7 @@ for infile in $IN_DIR/*.in; do
 
     # Run the command and store its output in a temporary file
     tmpfile=$(mktemp)
-    build/bin/repl < "$infile" > "$tmpfile" 2>&1
+    .lake/build/bin/repl < "$infile" > "$tmpfile" 2>&1
 
     # Compare the output with the expected output
     if diff "$tmpfile" "$expectedfile"; then

diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out
@@ -3,7 +3,7 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : Nat ⊢ x + 1 > x",
+   "goal": "x : Nat\n⊢ x + 1 > x",
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",

diff --git a/test/Mathlib/test/H20231115_2.expected.out b/test/Mathlib/test/H20231115_2.expected.out
@@ -3,11 +3,11 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 3, "column": 12},
-   "goal": "case zero ⊢ Nat.zero + 1 > Nat.zero",
+   "goal": "case zero\n⊢ Nat.zero + 1 > Nat.zero",
    "endPos": {"line": 3, "column": 17}},
   {"proofState": 1,
    "pos": {"line": 3, "column": 12},
-   "goal": "case succ x : Nat hx : x + 1 > x ⊢ Nat.succ x + 1 > Nat.succ x",
+   "goal": "case succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x",
    "endPos": {"line": 3, "column": 17}}],
  "messages":
  [{"severity": "warning",

diff --git a/test/invalid_tactic.expected.out b/test/invalid_tactic.expected.out
@@ -1,7 +1,7 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 43},
-   "goal": "x : Nat ⊢ x = x",
+   "goal": "x : Nat\n⊢ x = x",
    "endPos": {"line": 1, "column": 48}}],
  "messages":
  [{"severity": "warning",

diff --git a/test/readme.expected.out b/test/readme.expected.out
@@ -1,7 +1,7 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 29},
-   "goal": "x : Unit ⊢ Nat",
+   "goal": "x : Unit\n⊢ Nat",
    "endPos": {"line": 1, "column": 34}}],
  "messages":
  [{"severity": "warning",

diff --git a/test/variables.expected.out b/test/variables.expected.out
@@ -11,7 +11,7 @@
  [{"proofState": 0,
    "pos": {"line": 3, "column": 2},
    "goal":
-   "x y : Nat f : Nat → Nat h0 : f 5 = 3 h1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y)) ⊢ ∃ k, f 2015 = k",
+   "x y : Nat\nf : Nat → Nat\nh0 : f 5 = 3\nh1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))\n⊢ ∃ k, f 2015 = k",
    "endPos": {"line": 3, "column": 7}}],
  "messages":
  [{"severity": "warning",