diff --git a/lakefile.lean b/lakefile.lean index caec4b0..a241fa1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -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 @@ -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"