diff --git a/tests/bench/dag_hassorry_issue.lean b/tests/bench/dag_hassorry_issue.lean index 728cb8618c..2c32c0fc23 100644 --- a/tests/bench/dag_hassorry_issue.lean +++ b/tests/bench/dag_hassorry_issue.lean @@ -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 := "", fileMap := default } { env } + IO.println "ok" diff --git a/tests/bench/dag_hassorry_issue.lean.args b/tests/bench/dag_hassorry_issue.lean.args new file mode 100644 index 0000000000..1746da6312 --- /dev/null +++ b/tests/bench/dag_hassorry_issue.lean.args @@ -0,0 +1 @@ +10000 \ No newline at end of file diff --git a/tests/bench/dag_hassorry_issue.lean.expected.out b/tests/bench/dag_hassorry_issue.lean.expected.out new file mode 100644 index 0000000000..9766475a41 --- /dev/null +++ b/tests/bench/dag_hassorry_issue.lean.expected.out @@ -0,0 +1 @@ +ok