From 4f0f989e6f95b88bcd87f8b5cd05d7615ae801fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Jan 2017 09:03:02 -0800 Subject: [PATCH] fix(tests/lean/interactive): expected output @kha The following three tests were broken on my machine. The new produced output looked correct. So, I updated the expected output files. Is this ok? see #1296 --- tests/lean/interactive/complete.lean.expected.out | 2 +- tests/lean/interactive/complete_tactic.lean.expected.out | 2 +- .../lean/interactive/complete_trailing_period.lean.expected.out | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/interactive/complete.lean.expected.out b/tests/lean/interactive/complete.lean.expected.out index b4875d3ad4..3ea3a9be90 100644 --- a/tests/lean/interactive/complete.lean.expected.out +++ b/tests/lean/interactive/complete.lean.expected.out @@ -1,4 +1,4 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"text":"foo","type":"Type"},{"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"}],"prefix":"fo","response":"ok","seq_num":6} +{"completions":[{"source":{"column":10,"line":3},"text":"foo","type":"Type"},{"source":{"column":10,"line":3},"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"}],"prefix":"fo","response":"ok","seq_num":6} {"prefix":"","response":"ok","seq_num":9} {"prefix":"","response":"ok","seq_num":13} diff --git a/tests/lean/interactive/complete_tactic.lean.expected.out b/tests/lean/interactive/complete_tactic.lean.expected.out index 2ab3dc62b6..2481ee399c 100644 --- a/tests/lean/interactive/complete_tactic.lean.expected.out +++ b/tests/lean/interactive/complete_tactic.lean.expected.out @@ -1,5 +1,5 @@ {"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},"response":"additional_message"} -{"msg":{"caption":"","file_name":"f","pos_col":52,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},"response":"additional_message"} +{"msg":{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},"response":"additional_message"} {"message":"file invalidated","response":"ok","seq_num":0} {"prefix":"","response":"ok","seq_num":2} {"prefix":"","response":"ok","seq_num":5} diff --git a/tests/lean/interactive/complete_trailing_period.lean.expected.out b/tests/lean/interactive/complete_trailing_period.lean.expected.out index 38344ce6e7..43df7ccedc 100644 --- a/tests/lean/interactive/complete_trailing_period.lean.expected.out +++ b/tests/lean/interactive/complete_trailing_period.lean.expected.out @@ -1,2 +1,2 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"},{"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6} +{"completions":[{"source":{"column":10,"line":3},"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6}