From d800631a7b36b7195d83dd888c6a63183c95bf8a Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 1 Sep 2024 23:21:11 +0900
Subject: [PATCH] TEST: add release build option

---
 lakefile.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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"