From 93b074dbed157402dd3f311aa913e11d3cebf91e Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 13 Oct 2023 12:58:50 +1100 Subject: [PATCH] chore: newline after responses, for easier parsing --- .vscode/settings.json | 3 ++- REPL/Main.lean | 1 + test/def_eval.expected.out | 2 ++ test/enableInitializersExecution.expected.out | 1 + test/pickle_environment.expected.out | 4 ++++ test/pickle_environment_with_imports.expected.out | 5 +++++ test/pickle_proof_state_1.expected.out | 8 ++++++++ test/pickle_proof_state_2.expected.out | 2 ++ test/proof_step.expected.out | 4 ++++ test/synthesize_placeholder.expected.out | 1 + test/tactic_sorry.expected.out | 1 + test/term_sorry.expected.out | 1 + test/unfinished_tactic_block.expected.out | 1 + test/unknown_environment.expected.out | 1 + test/unknown_proof_state.expected.out | 2 ++ test/unknown_tactic.expected.out | 1 + 16 files changed, 37 insertions(+), 1 deletion(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 89f72cb..f358003 100644 --- a/.vscode/settings.json +++ b/.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, } diff --git a/REPL/Main.lean b/REPL/Main.lean index db9e8ea..f0136af 100644 --- a/REPL/Main.lean +++ b/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`. -/ diff --git a/test/def_eval.expected.out b/test/def_eval.expected.out index 83bef74..ca275fd 100644 --- a/test/def_eval.expected.out +++ b/test/def_eval.expected.out @@ -1,4 +1,5 @@ {"sorries": [], "messages": [], "env": 0} + {"sorries": [], "messages": [{"severity": "info", @@ -6,3 +7,4 @@ "endPos": {"line": 1, "column": 6}, "data": "rfl : f = f"}], "env": 1} + diff --git a/test/enableInitializersExecution.expected.out b/test/enableInitializersExecution.expected.out index bee2c06..7baaf7a 100644 --- a/test/enableInitializersExecution.expected.out +++ b/test/enableInitializersExecution.expected.out @@ -1 +1,2 @@ {"sorries": [], "messages": [], "env": 0} + diff --git a/test/pickle_environment.expected.out b/test/pickle_environment.expected.out index 5e0a145..40b4851 100644 --- a/test/pickle_environment.expected.out +++ b/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} + diff --git a/test/pickle_environment_with_imports.expected.out b/test/pickle_environment_with_imports.expected.out index 08f5fab..58bff0a 100644 --- a/test/pickle_environment_with_imports.expected.out +++ b/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} + diff --git a/test/pickle_proof_state_1.expected.out b/test/pickle_proof_state_1.expected.out index 2dea5fc..a3b9a32 100644 --- a/test/pickle_proof_state_1.expected.out +++ b/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": []} + diff --git a/test/pickle_proof_state_2.expected.out b/test/pickle_proof_state_2.expected.out index 387a23a..09a6bdf 100644 --- a/test/pickle_proof_state_2.expected.out +++ b/test/pickle_proof_state_2.expected.out @@ -1,2 +1,4 @@ {"proofState": 0, "goals": ["t : Nat\n⊢ Nat"]} + {"proofState": 1, "goals": []} + diff --git a/test/proof_step.expected.out b/test/proof_step.expected.out index cb909e2..2a26468 100644 --- a/test/proof_step.expected.out +++ b/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": []} + diff --git a/test/synthesize_placeholder.expected.out b/test/synthesize_placeholder.expected.out index 06119ac..46fafa5 100644 --- a/test/synthesize_placeholder.expected.out +++ b/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} + diff --git a/test/tactic_sorry.expected.out b/test/tactic_sorry.expected.out index 43fd2cb..0394d4f 100644 --- a/test/tactic_sorry.expected.out +++ b/test/tactic_sorry.expected.out @@ -9,3 +9,4 @@ "endPos": {"line": 1, "column": 5}, "data": "declaration uses 'sorry'"}], "env": 0} + diff --git a/test/term_sorry.expected.out b/test/term_sorry.expected.out index 71833dc..ab332e3 100644 --- a/test/term_sorry.expected.out +++ b/test/term_sorry.expected.out @@ -9,3 +9,4 @@ "endPos": {"line": 1, "column": 5}, "data": "declaration uses 'sorry'"}], "env": 0} + diff --git a/test/unfinished_tactic_block.expected.out b/test/unfinished_tactic_block.expected.out index 7df4f82..d5fac51 100644 --- a/test/unfinished_tactic_block.expected.out +++ b/test/unfinished_tactic_block.expected.out @@ -9,3 +9,4 @@ "endPos": {"line": 1, "column": 17}, "data": "unsolved goals\n⊢ Nat"}], "env": 0} + diff --git a/test/unknown_environment.expected.out b/test/unknown_environment.expected.out index 45a6e1c..9497cc5 100644 --- a/test/unknown_environment.expected.out +++ b/test/unknown_environment.expected.out @@ -1 +1,2 @@ {"message": "Unknown environment."} + diff --git a/test/unknown_proof_state.expected.out b/test/unknown_proof_state.expected.out index ccc3261..ee52464 100644 --- a/test/unknown_proof_state.expected.out +++ b/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."} + diff --git a/test/unknown_tactic.expected.out b/test/unknown_tactic.expected.out index 5b60a97..988daf0 100644 --- a/test/unknown_tactic.expected.out +++ b/test/unknown_tactic.expected.out @@ -9,4 +9,5 @@ "endPos": {"line": 1, "column": 5}, "data": "declaration uses 'sorry'"}], "env": 0} + uncaught exception: :1:1: unknown tactic