Skip to content

Commit 881a131

Browse files
authored
chore: re-enable tests (#10923)
1 parent fb3e2c1 commit 881a131

File tree

13 files changed

+39
-13
lines changed

13 files changed

+39
-13
lines changed

tests/bench/dag_hassorry_issue.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
import Lean
2-
def main : IO Unit := pure () #exit -- TODO: remove after stage0 update
32

43
open Lean
54

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
ok

tests/bench/liasolver.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ import Lean.Data.AssocList
77
import Std.Data.HashMap
88
import Std.Data.Iterators.Producers.Range
99
import Std.Data.Iterators.Combinators.StepSize
10-
def main : IO Unit := pure () #exit -- TODO: remove after stage0 update
1110

1211
open Lean
1312

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
SAT
2+
-104 -253 65 75 -271 269 234 -125 59 -291 23 -150 -127 -232 11 -66 -199 133 -51 -120 -141 276 24 6 -85 28 240 54 -182 -160 128 14 -212 269 -154 28 134 -125 -49 192 14 -130 69 -53 -157 264 103 48 -271 184

tests/compiler/escape.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
def main : IO Unit := pure () /- -- TODO: remove after stage0 update
21
def main : IO Unit := do
32
IO.eprintln $ "\rfailed at counter-example"
43
IO.eprintln $ "\tfailed at counter-example"
5-
-/

tests/compiler/escape.lean.expected.out

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
failed at counter-example
2+
failed at counter-example

tests/compiler/expr.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
import Lean
2-
def main : IO Unit := pure () /- -- TODO: remove after stage0 update
32

43
open Lean
54

@@ -9,4 +8,3 @@ IO.println e
98
IO.println s!"hash: {e.hash}"
109
IO.println e.getAppArgs
1110
pure 0
12-
-/
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
f a b
2+
hash: 2008687407
3+
#[a, b]

tests/compiler/str.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
def main : IO Unit := pure () /- -- TODO: remove after stage0 update
21
def showChars : Nat → String → String.Pos.Raw → IO Unit
32
| 0, _, _ => pure ()
43
| n+1, s, idx => do
@@ -28,4 +27,3 @@ IO.println ("ab".isPrefixOf "a") *>
2827
IO.println ("αb".isPrefixOf "αbc") *>
2928
IO.println ("\x00a").length *>
3029
pure 0
31-
-/
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
hello α_world_β
2+
llo α_world_β
3+
llo α_world_β
4+
llo α_world_
5+
6+
_world_β
7+
17
8+
"aaa"
9+
>> h
10+
>> e
11+
>> l
12+
>> l
13+
>> o
14+
>>
15+
>> α
16+
>> _
17+
>> w
18+
>> o
19+
>> r
20+
>> l
21+
>> d
22+
>> _
23+
>> β
24+
true
25+
true
26+
true
27+
true
28+
false
29+
false
30+
true
31+
2

0 commit comments

Comments
 (0)