chore: improve test
This commit is contained in:
parent
6d857a93b5
commit
fd0549feb5
3 changed files with 8 additions and 1 deletions
|
|
@ -49,4 +49,9 @@ def test (n : Nat) : CoreM Unit := do
|
|||
}
|
||||
return ()
|
||||
|
||||
#eval test 10000
|
||||
def main (args : List String) : IO Unit := do
|
||||
let [size] := args | throw (IO.userError s!"unexpected number of arguments, numeral expected")
|
||||
initSearchPath (← findSysroot)
|
||||
let env ← importModules [{ module := `Init.Prelude }] {} 0
|
||||
discard <| test size.toNat! |>.toIO { fileName := "<test>", fileMap := default } { env }
|
||||
IO.println "ok"
|
||||
|
|
|
|||
1
tests/bench/dag_hassorry_issue.lean.args
Normal file
1
tests/bench/dag_hassorry_issue.lean.args
Normal file
|
|
@ -0,0 +1 @@
|
|||
10000
|
||||
1
tests/bench/dag_hassorry_issue.lean.expected.out
Normal file
1
tests/bench/dag_hassorry_issue.lean.expected.out
Normal file
|
|
@ -0,0 +1 @@
|
|||
ok
|
||||
Loading…
Add table
Reference in a new issue