From fe774a25cfd9fb79bb87e34089284d6503d1a852 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Jun 2017 10:56:09 -0700 Subject: [PATCH] chore(tests/lean/interactive): fix tests --- tests/lean/interactive/complete.lean.expected.out | 2 +- tests/lean/interactive/hole4.lean.expected.out | 2 +- tests/lean/interactive/info.lean.expected.out | 2 +- tests/lean/interactive/info_id_pre_elab.lean.expected.out | 2 +- tests/lean/interactive/rb_map_ts.lean.expected.out | 6 +++--- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/lean/interactive/complete.lean.expected.out b/tests/lean/interactive/complete.lean.expected.out index eae1805cd8..2f3c418ead 100644 --- a/tests/lean/interactive/complete.lean.expected.out +++ b/tests/lean/interactive/complete.lean.expected.out @@ -1,4 +1,4 @@ -{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":19,"severity":"information","text":"inductive foo : Type\nconstructors:"}],"response":"all_messages"} +{"msgs":[{"caption":"print result","end_pos_col":0,"end_pos_line":22,"file_name":"f","pos_col":0,"pos_line":19,"severity":"information","text":"inductive foo : Type\nconstructors:"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"completions":[{"source":,"text":"foo","type":"Type"},{"source":{"column":10,"line":3},"text":"foo.rec","type":"Π (C : foo → Sort l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (C : foo → Sort l) (n : foo), C n"}],"prefix":"fo","response":"ok","seq_num":6} {"response":"ok","seq_num":10} diff --git a/tests/lean/interactive/hole4.lean.expected.out b/tests/lean/interactive/hole4.lean.expected.out index 8a2740dd29..06122fd65f 100644 --- a/tests/lean/interactive/hole4.lean.expected.out +++ b/tests/lean/interactive/hole4.lean.expected.out @@ -1,3 +1,3 @@ {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"warning","text":"declaration 'x' uses sorry"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} -{"replacements":{"alternatives":[{"code":"λ (a : ℕ), {! !}","description":""}],"end":{"column":16,"line":2},"file":"f","start":{"column":0,"line":2}},"response":"ok","seq_num":3} +{"replacements":{"alternatives":[{"code":"λ (a : ℕ), {! !}","description":""}],"end":{"column":12,"line":2},"file":"f","start":{"column":0,"line":2}},"response":"ok","seq_num":3} diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out index a280a6d661..38d909d724 100644 --- a/tests/lean/interactive/info.lean.expected.out +++ b/tests/lean/interactive/info.lean.expected.out @@ -1,4 +1,4 @@ -{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"} +{"msgs":[{"caption":"print result","end_pos_col":26,"end_pos_line":19,"file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"source":},"response":"ok","seq_num":2} {"record":{"doc":"reducible"},"response":"ok","seq_num":5} diff --git a/tests/lean/interactive/info_id_pre_elab.lean.expected.out b/tests/lean/interactive/info_id_pre_elab.lean.expected.out index 6bff823109..f2e851353a 100644 --- a/tests/lean/interactive/info_id_pre_elab.lean.expected.out +++ b/tests/lean/interactive/info_id_pre_elab.lean.expected.out @@ -1,7 +1,7 @@ {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"} {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"}],"response":"all_messages"} {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"} -{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","file_name":"f","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (abstract tac none) : tactic unit → tactic unit"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n trace\n tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","end_pos_col":27,"end_pos_line":7,"file_name":"f","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (abstract tac none) : tactic unit → tactic unit"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"response":"ok","seq_num":4} {"record":{"full-id":"tactic.abstract","source":,"type":"tactic unit → opt_param (option name) none → opt_param bool tt → tactic unit"},"response":"ok","seq_num":7} diff --git a/tests/lean/interactive/rb_map_ts.lean.expected.out b/tests/lean/interactive/rb_map_ts.lean.expected.out index 38d644e504..a70e476d9f 100644 --- a/tests/lean/interactive/rb_map_ts.lean.expected.out +++ b/tests/lean/interactive/rb_map_ts.lean.expected.out @@ -1,7 +1,7 @@ {"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"} -{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"} +{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":89,"file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":67} {"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":71}