From d0f61b7ce2728b9ef2a24b0fec9a048518fada6f Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 9 Sep 2024 19:47:51 +0900
Subject: [PATCH] =?UTF-8?q?`lake=20run=20build`=20=E3=81=AE=E5=AE=9F?=
 =?UTF-8?q?=E8=A1=8C=E3=81=8C=E9=81=85=E3=81=84=E3=81=AE=E3=81=A7=E4=BB=A3?=
 =?UTF-8?q?=E6=9B=BF=E6=89=8B=E6=AE=B5=E3=82=92=E7=94=A8=E6=84=8F=E3=81=99?=
 =?UTF-8?q?=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

see #686
---
 lakefile.lean     | 13 +++++--------
 scripts/Build.ps1 | 10 ++++++++++
 2 files changed, 15 insertions(+), 8 deletions(-)
 create mode 100644 scripts/Build.ps1

diff --git a/lakefile.lean b/lakefile.lean
index f2438beb..3f232d85 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -25,12 +25,12 @@ lean_lib Examples where
 section Script
 
 /-- 与えられた文字列をシェルで実行する -/
-@[inline] def runCmd (input : String) : IO Unit := do
+def runCmd (input : String) : IO Unit := do
   let cmdList := input.splitOn " "
   let cmd := cmdList.head!
   let args := cmdList.tail |>.toArray
   let out ← IO.Process.output {
-    cmd  := cmd
+    cmd := cmd
     args := args
   }
   if out.exitCode != 0 then
@@ -55,10 +55,10 @@ macro_rules
     IO.println s!"Running {$s}: {end_time - start_time}ms")
 
 /-- mk_exercise と mdgen と mdbook を順に実行し、
-Lean ファイルから Markdown ファイルと HTML ファイルを生成する。-/
-script build do
-  let start_time ← IO.monoMsNow;
+Lean ファイルから Markdown ファイルと HTML ファイルを生成する。
 
+`.\scripts\Build.ps1` を実行したほうが高速 -/
+script build do
   -- `lake run mk_exercise` を使用すると遅くなってしまうのでコピペしている
   with_time running "mk_exercise"
     runCmd "lake exe mk_exercise Examples/Solution Exercise"
@@ -69,9 +69,6 @@ script build do
 
   with_time running "mdbook"
     runCmd "mdbook build"
-
-  let end_time ← IO.monoMsNow;
-  IO.println s!"Total time: {end_time - start_time}ms"
   return 0
 
 end Script
diff --git a/scripts/Build.ps1 b/scripts/Build.ps1
new file mode 100644
index 00000000..84483967
--- /dev/null
+++ b/scripts/Build.ps1
@@ -0,0 +1,10 @@
+<# lake run build に相当するスクリプト
+
+lake を介することで実行が遅くなってしまうので、
+lake を介することなく実行ファイルを直接叩く。 #>
+
+./.lake/packages/mk-exercise/.lake/build/bin/mk_exercise.exe Examples/Solution Exercise
+
+./.lake/packages/mdgen/.lake/build/bin/mdgen.exe Exercise src/Exercise
+
+mdbook build