max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/lean/interactive): expected output

Browse source 
@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
This commit is contained in:
Leonardo de Moura 2017-01-10 09:03:02 -08:00
parent 80d0b8d5f5
commit 4f0f989e6f
3 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/complete.lean.expected.out
View file

@ -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}

2
tests/lean/interactive/complete_tactic.lean.expected.out
View file

@ -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}

2
tests/lean/interactive/complete_trailing_period.lean.expected.out
View file

@ -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}