chore: newline after responses, for easier parsing

.vscode/settings.json

@@ -5,6 +5,7 @@
   "files.encoding": "utf8",
   "files.eol": "\n",
   "files.insertFinalNewline": true,
-  "files.trimFinalNewlines": true,
+  // We don't use this: it messes up our test files!
+  // "files.trimFinalNewlines": true,
   "files.trimTrailingWhitespace": true,
 }

REPL/Main.lean

@@ -224,6 +224,7 @@ where loop : M IO Unit := do
   | .unpickleEnvironment r => return toJson (← unpickleEnvironment r)
   | .pickleProofState r => return toJson (← pickleProofState r)
   | .unpickleProofState r => return toJson (← unpickleProofState r)
+  IO.println "" -- easier to parse the output if there are blank lines
   loop
 
 /-- Main executable function, run as `lake exe repl`. -/

test/def_eval.expected.out

@@ -1,8 +1,10 @@
 {"sorries": [], "messages": [], "env": 0}
+
 {"sorries": [],
  "messages":
  [{"severity": "info",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 6},
    "data": "rfl : f = f"}],
  "env": 1}
+

test/enableInitializersExecution.expected.out

@@ -1 +1,2 @@
 {"sorries": [], "messages": [], "env": 0}
+

test/pickle_environment.expected.out

@@ -1,4 +1,8 @@
 {"sorries": [], "messages": [], "env": 0}
+
 {"sorries": [], "messages": [], "env": 0}
+
 {"sorries": [], "messages": [], "env": 1}
+
 {"sorries": [], "messages": [], "env": 2}
+

test/pickle_environment_with_imports.expected.out

@@ -1,5 +1,10 @@
 {"sorries": [], "messages": [], "env": 0}
+
 {"sorries": [], "messages": [], "env": 1}
+
 {"sorries": [], "messages": [], "env": 1}
+
 {"sorries": [], "messages": [], "env": 2}
+
 {"sorries": [], "messages": [], "env": 3}
+

test/pickle_proof_state_1.expected.out

@@ -1,4 +1,5 @@
 {"sorries": [], "messages": [], "env": 0}
+
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
@@ -10,9 +11,16 @@
    "endPos": {"line": 1, "column": 5},
    "data": "declaration uses 'sorry'"}],
  "env": 1}
+
 {"proofState": 1, "goals": ["⊢ Nat"]}
+
 {"proofState": 2, "goals": ["⊢ Nat"]}
+
 {"proofState": 3, "goals": ["t : Nat\n⊢ Nat"]}
+
 {"proofState": 4, "goals": ["t : Nat\n⊢ Nat"]}
+
 {"proofState": 5, "goals": ["t : Nat\n⊢ Nat"]}
+
 {"proofState": 6, "goals": []}
+

test/pickle_proof_state_2.expected.out

@@ -1,2 +1,4 @@
 {"proofState": 0, "goals": ["t : Nat\n⊢ Nat"]}
+
 {"proofState": 1, "goals": []}
+

test/proof_step.expected.out

@@ -9,6 +9,10 @@
    "endPos": {"line": 1, "column": 5},
    "data": "declaration uses 'sorry'"}],
  "env": 0}
+
 {"proofState": 1, "goals": ["⊢ Int"]}
+
 {"proofState": 2, "goals": ["t : Nat\n⊢ Nat"]}
+
 {"proofState": 3, "goals": []}
+

test/synthesize_placeholder.expected.out

@@ -5,3 +5,4 @@
    "endPos": {"line": 1, "column": 16},
    "data": "don't know how to synthesize placeholder\ncontext:\n⊢ Nat"}],
  "env": 0}
+

test/tactic_sorry.expected.out

@@ -9,3 +9,4 @@
    "endPos": {"line": 1, "column": 5},
    "data": "declaration uses 'sorry'"}],
  "env": 0}
+

test/term_sorry.expected.out

@@ -9,3 +9,4 @@
    "endPos": {"line": 1, "column": 5},
    "data": "declaration uses 'sorry'"}],
  "env": 0}
+

test/unfinished_tactic_block.expected.out

@@ -9,3 +9,4 @@
    "endPos": {"line": 1, "column": 17},
    "data": "unsolved goals\n⊢ Nat"}],
  "env": 0}
+

test/unknown_environment.expected.out

@@ -1 +1,2 @@
 {"message": "Unknown environment."}
+

test/unknown_proof_state.expected.out

@@ -9,4 +9,6 @@
    "endPos": {"line": 1, "column": 5},
    "data": "declaration uses 'sorry'"}],
  "env": 0}
+
 {"message": "Unknown proof state."}
+

test/unknown_tactic.expected.out

@@ -9,4 +9,5 @@
    "endPos": {"line": 1, "column": 5},
    "data": "declaration uses 'sorry'"}],
  "env": 0}
+
 uncaught exception: <input>:1:1: unknown tactic