Skip to content
This repository was archived by the owner on Aug 24, 2024. It is now read-only.

Commit 0488054

Browse files
insightmindinsightmind
committed
fix: use verbose output for tests
This is to simplify diffing and make it easier to validate changes in the output.
1 parent 0c4d564 commit 0488054

21 files changed

+72765
-20
lines changed

‎test/bench/Basic.lean.leanInk.expected

Lines changed: 50905 additions & 1 deletion
Large diffs are not rendered by default.

‎test/bugs/GH_15.lean.leanInk.expected

Lines changed: 136 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,136 @@
1-
[{"contents":[{"typeinfo":{"type":"Nat → Nat","name":"example","_type":"typeinfo"},"semanticType":"Keyword","raw":"example","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Type","name":"Nat","_type":"typeinfo"},"semanticType":null,"raw":"Nat","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" → ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Type","name":"Nat","_type":"typeinfo"},"semanticType":null,"raw":"Nat","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":"\n | ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"0","_type":"typeinfo"},"semanticType":null,"raw":"0","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" => ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"0","_type":"typeinfo"},"semanticType":null,"raw":"0","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":"\n | ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"n","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"n","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" + ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"1","_type":"typeinfo"},"semanticType":null,"raw":"1","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" => ","link":null,"docstring":null,"_type":"token"}],"_type":"text"},{"messages":[],"goals":[{"name":"","hypotheses":[{"type":"Nat","names":["n"],"body":"","_type":"hypothesis"}],"conclusion":"Nat","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"by","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"messages":[],"goals":[{"name":"","hypotheses":[],"conclusion":"Goals accomplished! 🐙","_type":"goal"}],"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"exact","link":null,"docstring":"`exact e` closes the main goal if its target type matches that of `e`.\n","_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":"`exact e` closes the main goal if its target type matches that of `e`.\n","_type":"token"},{"typeinfo":{"type":"Nat","name":"n","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"n","link":null,"docstring":null,"_type":"token"}],"_type":"sentence"},{"contents":[],"_type":"text"}]
1+
[{"contents":
2+
[{"typeinfo": {"type": "Nat → Nat", "name": "example", "_type": "typeinfo"},
3+
"semanticType": "Keyword",
4+
"raw": "example",
5+
"link": null,
6+
"docstring": null,
7+
"_type": "token"},
8+
{"typeinfo": null,
9+
"semanticType": null,
10+
"raw": " : ",
11+
"link": null,
12+
"docstring": null,
13+
"_type": "token"},
14+
{"typeinfo": {"type": "Type", "name": "Nat", "_type": "typeinfo"},
15+
"semanticType": null,
16+
"raw": "Nat",
17+
"link": null,
18+
"docstring": null,
19+
"_type": "token"},
20+
{"typeinfo": null,
21+
"semanticType": null,
22+
"raw": " → ",
23+
"link": null,
24+
"docstring": null,
25+
"_type": "token"},
26+
{"typeinfo": {"type": "Type", "name": "Nat", "_type": "typeinfo"},
27+
"semanticType": null,
28+
"raw": "Nat",
29+
"link": null,
30+
"docstring": null,
31+
"_type": "token"},
32+
{"typeinfo": null,
33+
"semanticType": null,
34+
"raw": "\n | ",
35+
"link": null,
36+
"docstring": null,
37+
"_type": "token"},
38+
{"typeinfo": {"type": "Nat", "name": "0", "_type": "typeinfo"},
39+
"semanticType": null,
40+
"raw": "0",
41+
"link": null,
42+
"docstring": null,
43+
"_type": "token"},
44+
{"typeinfo": null,
45+
"semanticType": null,
46+
"raw": " => ",
47+
"link": null,
48+
"docstring": null,
49+
"_type": "token"},
50+
{"typeinfo": {"type": "Nat", "name": "0", "_type": "typeinfo"},
51+
"semanticType": null,
52+
"raw": "0",
53+
"link": null,
54+
"docstring": null,
55+
"_type": "token"},
56+
{"typeinfo": null,
57+
"semanticType": null,
58+
"raw": "\n | ",
59+
"link": null,
60+
"docstring": null,
61+
"_type": "token"},
62+
{"typeinfo": {"type": "Nat", "name": "n", "_type": "typeinfo"},
63+
"semanticType": "Name.Variable",
64+
"raw": "n",
65+
"link": null,
66+
"docstring": null,
67+
"_type": "token"},
68+
{"typeinfo": null,
69+
"semanticType": null,
70+
"raw": " + ",
71+
"link": null,
72+
"docstring": null,
73+
"_type": "token"},
74+
{"typeinfo": {"type": "Nat", "name": "1", "_type": "typeinfo"},
75+
"semanticType": null,
76+
"raw": "1",
77+
"link": null,
78+
"docstring": null,
79+
"_type": "token"},
80+
{"typeinfo": null,
81+
"semanticType": null,
82+
"raw": " => ",
83+
"link": null,
84+
"docstring": null,
85+
"_type": "token"}],
86+
"_type": "text"},
87+
{"messages": [],
88+
"goals":
89+
[{"name": "",
90+
"hypotheses":
91+
[{"type": "Nat", "names": ["n"], "body": "", "_type": "hypothesis"}],
92+
"conclusion": "Nat",
93+
"_type": "goal"}],
94+
"contents":
95+
[{"typeinfo": null,
96+
"semanticType": "Keyword",
97+
"raw": "by",
98+
"link": null,
99+
"docstring": null,
100+
"_type": "token"},
101+
{"typeinfo": null,
102+
"semanticType": null,
103+
"raw": " ",
104+
"link": null,
105+
"docstring": null,
106+
"_type": "token"}],
107+
"_type": "sentence"},
108+
{"messages": [],
109+
"goals":
110+
[{"name": "",
111+
"hypotheses": [],
112+
"conclusion": "Goals accomplished! 🐙",
113+
"_type": "goal"}],
114+
"contents":
115+
[{"typeinfo": null,
116+
"semanticType": "Keyword",
117+
"raw": "exact",
118+
"link": null,
119+
"docstring":
120+
"`exact e` closes the main goal if its target type matches that of `e`.\n",
121+
"_type": "token"},
122+
{"typeinfo": null,
123+
"semanticType": null,
124+
"raw": " ",
125+
"link": null,
126+
"docstring":
127+
"`exact e` closes the main goal if its target type matches that of `e`.\n",
128+
"_type": "token"},
129+
{"typeinfo": {"type": "Nat", "name": "n", "_type": "typeinfo"},
130+
"semanticType": "Name.Variable",
131+
"raw": "n",
132+
"link": null,
133+
"docstring": null,
134+
"_type": "token"}],
135+
"_type": "sentence"},
136+
{"contents": [], "_type": "text"}]

‎test/dep/Dep.lean.leanInk.expected

Lines changed: 3106 additions & 1 deletion
Large diffs are not rendered by default.

‎test/dep/Main.lean.leanInk.expected

Lines changed: 80 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,80 @@
1-
[{"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"def","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"IO Unit","name":"main","_type":"typeinfo"},"semanticType":null,"raw":"main","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Type → Type","name":"IO","_type":"typeinfo"},"semanticType":null,"raw":"IO","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Type","name":"Unit","_type":"typeinfo"},"semanticType":null,"raw":"Unit","link":null,"docstring":"An abbreviation for `PUnit.{0}`, its most common instantiation.\n This Type should be preferred over `PUnit` where possible to avoid\n unnecessary universe parameters. ","_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" :=\n ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"{α : Type} → [inst : ToString α] → α → IO Unit","name":"IO.println","_type":"typeinfo"},"semanticType":null,"raw":"IO.println","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"String","name":"s!\"Hello, world!\"","_type":"typeinfo"},"semanticType":"Keyword","raw":"s!","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"String","name":"s!\"Hello, world!\"","_type":"typeinfo"},"semanticType":null,"raw":"\"Hello, world!\"","link":null,"docstring":null,"_type":"token"}],"_type":"text"}]
1+
[{"contents":
2+
[{"typeinfo": null,
3+
"semanticType": "Keyword",
4+
"raw": "def",
5+
"link": null,
6+
"docstring": null,
7+
"_type": "token"},
8+
{"typeinfo": null,
9+
"semanticType": null,
10+
"raw": " ",
11+
"link": null,
12+
"docstring": null,
13+
"_type": "token"},
14+
{"typeinfo": {"type": "IO Unit", "name": "main", "_type": "typeinfo"},
15+
"semanticType": null,
16+
"raw": "main",
17+
"link": null,
18+
"docstring": null,
19+
"_type": "token"},
20+
{"typeinfo": null,
21+
"semanticType": null,
22+
"raw": " : ",
23+
"link": null,
24+
"docstring": null,
25+
"_type": "token"},
26+
{"typeinfo": {"type": "Type → Type", "name": "IO", "_type": "typeinfo"},
27+
"semanticType": null,
28+
"raw": "IO",
29+
"link": null,
30+
"docstring": null,
31+
"_type": "token"},
32+
{"typeinfo": null,
33+
"semanticType": null,
34+
"raw": " ",
35+
"link": null,
36+
"docstring": null,
37+
"_type": "token"},
38+
{"typeinfo": {"type": "Type", "name": "Unit", "_type": "typeinfo"},
39+
"semanticType": null,
40+
"raw": "Unit",
41+
"link": null,
42+
"docstring":
43+
"An abbreviation for `PUnit.{0}`, its most common instantiation.\n This Type should be preferred over `PUnit` where possible to avoid\n unnecessary universe parameters. ",
44+
"_type": "token"},
45+
{"typeinfo": null,
46+
"semanticType": null,
47+
"raw": " :=\n ",
48+
"link": null,
49+
"docstring": null,
50+
"_type": "token"},
51+
{"typeinfo":
52+
{"type": "{α : Type} → [inst : ToString α] → α → IO Unit",
53+
"name": "IO.println",
54+
"_type": "typeinfo"},
55+
"semanticType": null,
56+
"raw": "IO.println",
57+
"link": null,
58+
"docstring": null,
59+
"_type": "token"},
60+
{"typeinfo": null,
61+
"semanticType": null,
62+
"raw": " ",
63+
"link": null,
64+
"docstring": null,
65+
"_type": "token"},
66+
{"typeinfo":
67+
{"type": "String", "name": "s!\"Hello, world!\"", "_type": "typeinfo"},
68+
"semanticType": "Keyword",
69+
"raw": "s!",
70+
"link": null,
71+
"docstring": null,
72+
"_type": "token"},
73+
{"typeinfo":
74+
{"type": "String", "name": "s!\"Hello, world!\"", "_type": "typeinfo"},
75+
"semanticType": null,
76+
"raw": "\"Hello, world!\"",
77+
"link": null,
78+
"docstring": null,
79+
"_type": "token"}],
80+
"_type": "text"}]

‎test/playground/Function.lean.leanInk.expected

Lines changed: 8299 additions & 1 deletion
Large diffs are not rendered by default.

‎test/playground/Simple.lean.leanInk.expected

Lines changed: 80 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,80 @@
1-
[{"contents":[{"typeinfo":null,"semanticType":"Keyword","raw":"def","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat → Nat → Nat","name":"add","_type":"typeinfo"},"semanticType":null,"raw":"add","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" (","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"x","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"x","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"y","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"y","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" : ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Type","name":"Nat","_type":"typeinfo"},"semanticType":null,"raw":"Nat","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":") := ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"x","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"x","link":null,"docstring":null,"_type":"token"},{"typeinfo":null,"semanticType":null,"raw":" + ","link":null,"docstring":null,"_type":"token"},{"typeinfo":{"type":"Nat","name":"y","_type":"typeinfo"},"semanticType":"Name.Variable","raw":"y","link":null,"docstring":null,"_type":"token"}],"_type":"text"}]
1+
[{"contents":
2+
[{"typeinfo": null,
3+
"semanticType": "Keyword",
4+
"raw": "def",
5+
"link": null,
6+
"docstring": null,
7+
"_type": "token"},
8+
{"typeinfo": null,
9+
"semanticType": null,
10+
"raw": " ",
11+
"link": null,
12+
"docstring": null,
13+
"_type": "token"},
14+
{"typeinfo": {"type": "Nat → Nat → Nat", "name": "add", "_type": "typeinfo"},
15+
"semanticType": null,
16+
"raw": "add",
17+
"link": null,
18+
"docstring": null,
19+
"_type": "token"},
20+
{"typeinfo": null,
21+
"semanticType": null,
22+
"raw": " (",
23+
"link": null,
24+
"docstring": null,
25+
"_type": "token"},
26+
{"typeinfo": {"type": "Nat", "name": "x", "_type": "typeinfo"},
27+
"semanticType": "Name.Variable",
28+
"raw": "x",
29+
"link": null,
30+
"docstring": null,
31+
"_type": "token"},
32+
{"typeinfo": null,
33+
"semanticType": null,
34+
"raw": " ",
35+
"link": null,
36+
"docstring": null,
37+
"_type": "token"},
38+
{"typeinfo": {"type": "Nat", "name": "y", "_type": "typeinfo"},
39+
"semanticType": "Name.Variable",
40+
"raw": "y",
41+
"link": null,
42+
"docstring": null,
43+
"_type": "token"},
44+
{"typeinfo": null,
45+
"semanticType": null,
46+
"raw": " : ",
47+
"link": null,
48+
"docstring": null,
49+
"_type": "token"},
50+
{"typeinfo": {"type": "Type", "name": "Nat", "_type": "typeinfo"},
51+
"semanticType": null,
52+
"raw": "Nat",
53+
"link": null,
54+
"docstring": null,
55+
"_type": "token"},
56+
{"typeinfo": null,
57+
"semanticType": null,
58+
"raw": ") := ",
59+
"link": null,
60+
"docstring": null,
61+
"_type": "token"},
62+
{"typeinfo": {"type": "Nat", "name": "x", "_type": "typeinfo"},
63+
"semanticType": "Name.Variable",
64+
"raw": "x",
65+
"link": null,
66+
"docstring": null,
67+
"_type": "token"},
68+
{"typeinfo": null,
69+
"semanticType": null,
70+
"raw": " + ",
71+
"link": null,
72+
"docstring": null,
73+
"_type": "token"},
74+
{"typeinfo": {"type": "Nat", "name": "y", "_type": "typeinfo"},
75+
"semanticType": "Name.Variable",
76+
"raw": "y",
77+
"link": null,
78+
"docstring": null,
79+
"_type": "token"}],
80+
"_type": "text"}]

‎test/playground/infoTree.lean.leanInk.expected

Lines changed: 1312 additions & 1 deletion
Large diffs are not rendered by default.

‎test/playground/playground_1.lean.leanInk.expected

Lines changed: 2601 additions & 1 deletion
Large diffs are not rendered by default.

0 commit comments

Comments
 (0)