Skip to content

Commit

Permalink
TEST: add release build option
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Sep 1, 2024
1 parent ce84564 commit d800631
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ open Lake DSL

package «mk-exercise» where
-- add package configuration options here
preferReleaseBuild := true

lean_lib «MkExercise» where
-- add library configuration options here
Expand Down Expand Up @@ -34,7 +35,10 @@ macro "with_time" x:doElem : doElem => `(doElem| do

/-- run test by `lake test` -/
@[test_driver] script test do
IO.print "performance test "
IO.print "time of running the exe file: "
with_time runCmd ".lake/build/bin/mk_exercise.exe Test/Performance Test/Out"

IO.print "time of running `lake exe`: "
with_time runCmd "lake exe mk_exercise Test/Performance Test/Out"

runCmd "lake exe mk_exercise Test/Src Test/Out"
Expand Down

0 comments on commit d800631

Please sign in to comment.