From a591e35544bc594778888cdb2a70300ae84522db Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 13 Mar 2017 09:24:42 +0100 Subject: [PATCH] chore(*): fix tests --- src/tests/shell/.gitignore | 1 + src/tests/shell/shell_test.expected.out | 2 +- tests/lean/interactive/info.lean.expected.out | 2 +- tests/lean/unification_hints2.lean.expected.out | 4 ++-- 4 files changed, 5 insertions(+), 4 deletions(-) create mode 100644 src/tests/shell/.gitignore diff --git a/src/tests/shell/.gitignore b/src/tests/shell/.gitignore new file mode 100644 index 0000000000..4cf1a84d6e --- /dev/null +++ b/src/tests/shell/.gitignore @@ -0,0 +1 @@ +*.produced.out diff --git a/src/tests/shell/shell_test.expected.out b/src/tests/shell/shell_test.expected.out index 6e510c135c..7cd72b2568 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,"line":1},"type":"Type"},"response":"ok","seq_num":1} +{"record":{"full-id":"f","source":{"column":10,"file":"f","line":1},"type":"Type"},"response":"ok","seq_num":1} diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out index e02ab44e11..25037c8633 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":"@[reducible]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"} +{"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"} {"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/unification_hints2.lean.expected.out b/tests/lean/unification_hints2.lean.expected.out index ddb1c3e859..89b99cee35 100644 --- a/tests/lean/unification_hints2.lean.expected.out +++ b/tests/lean/unification_hints2.lean.expected.out @@ -1,10 +1,10 @@ m n : ℕ, i : F m ⊢ F.raise (succ n) m i = F.suc (m + n) (F.raise n m i) -unification_hints2.lean:7:8: warning: declaration '_example' uses sorry +unification_hints2.lean:7:0: warning: declaration '[anonymous]' uses sorry α : Type u, a b : α, l₁ l₂ : list α, i : G α l₂ ⊢ G.raise α (a :: l₁) l₂ i = G.cons α a (l₁ ++ l₂) (G.raise α l₁ l₂ i) -unification_hints2.lean:24:8: warning: declaration '_example' uses sorry +unification_hints2.lean:24:0: warning: declaration '[anonymous]' uses sorry