From d90dda01b07f39b819cd82a03fd32d742e27eaeb Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 20 Mar 2017 09:15:13 +0100 Subject: [PATCH] chore(*): fix tests --- src/tests/shell/shell_test.expected.out | 2 +- tests/lean/interactive/do_info.lean.expected.out | 4 ++-- tests/lean/interactive/info_tactic.lean.expected.out | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tests/shell/shell_test.expected.out b/src/tests/shell/shell_test.expected.out index 7cd72b2568..6e510c135c 100644 --- a/src/tests/shell/shell_test.expected.out +++ b/src/tests/shell/shell_test.expected.out @@ -1,2 +1,2 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"full-id":"f","source":{"column":10,"file":"f","line":1},"type":"Type"},"response":"ok","seq_num":1} +{"record":{"full-id":"f","source":{"column":10,"line":1},"type":"Type"},"response":"ok","seq_num":1} diff --git a/tests/lean/interactive/do_info.lean.expected.out b/tests/lean/interactive/do_info.lean.expected.out index 163620dfa7..b3e538d180 100644 --- a/tests/lean/interactive/do_info.lean.expected.out +++ b/tests/lean/interactive/do_info.lean.expected.out @@ -1,7 +1,7 @@ {"msgs":[{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"full-id":"tactic.intro","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6} -{"record":{"full-id":"tactic.transitivity","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"opt_param tactic.transparency tactic.transparency.semireducible → tactic unit"},"response":"ok","seq_num":9} +{"record":{"full-id":"tactic.transitivity","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"opt_param transparency transparency.semireducible → tactic unit"},"response":"ok","seq_num":9} {"record":{"full-id":"tactic.assumption","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12} -{"record":{"full-id":"tactic.symmetry","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"opt_param tactic.transparency tactic.transparency.semireducible → tactic unit"},"response":"ok","seq_num":14} +{"record":{"full-id":"tactic.symmetry","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"opt_param transparency transparency.semireducible → tactic unit"},"response":"ok","seq_num":14} {"record":{"full-id":"tactic.assumption","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16} diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out index b10b43b1a5..3eaaf0ea57 100644 --- a/tests/lean/interactive/info_tactic.lean.expected.out +++ b/tests/lean/interactive/info_tactic.lean.expected.out @@ -1,4 +1,4 @@ -{"msg":{"caption":"","file_name":"f","pos_col":2,"pos_line":3,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"},"response":"additional_message"} +{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":3,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"state":"⊢ false","tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":4} {"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default} → tactic unit"},"response":"ok","seq_num":6}