lake run build の mk_exercise を実行する部分が遅い

[Seasawher]

mk_exercise のリポジトリで lake run test を実行したとき：

mk-exercise on  main
❯ lake run test
performance test 279ms

lean-by-example のリポジトリで lake run build を実行したとき：

lean-by-example on  main [$]
❯ lake run build
Running mk_exercise: 618ms
Running mdgen: 1370ms
Running mdbook: 773ms

このように、２倍以上の時間がなぜかかかるようになってしまう…。なぜ？？？？

(mk_exercise のリポジトリにおけるパフォーマンステストには、lean-by-example のものと同じファイルを使用している）

---

Zulip: Omit compilation and run the executable binary in the .lake

[Seasawher]

実行バイナリを .lake ディレクトリから拾ってくるとかなり速くなるが、CI 上でエラーになるようだ

section Script

/-- 与えられた文字列をシェルで実行する -/
@[inline] 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
    args := args
  }
  if out.exitCode != 0 then
    IO.eprintln out.stderr
    throw <| IO.userError s!"Failed to execute: {input}"
  else if !out.stdout.isEmpty then
    IO.println out.stdout

/-- mk_exercise を実行し、演習問題の解答に
解答部分を sorry に置き換えるなどの処理を施して演習問題ファイルを生成する。-/
script mk_exercise do
  runCmd "lake exe mk_exercise Examples/Solution Exercise"
  return 0

syntax (name := with_time) "with_time" "running" str doElem : doElem

macro_rules
  | `(doElem| with_time running $s $x) => `(doElem| do
    let start_time ← IO.monoMsNow;
    $x;
    let end_time ← IO.monoMsNow;
    IO.println s!"Running {$s}: {end_time - start_time}ms")

open System FilePath

/-- コンパイル済みのバイナリを取得する

* pkg: パッケージ名
* exeFile: 拡張子を除いた実行ファイル名
-/
def getBinary (pkg : String) (exeFile : String) : BaseIO String := do
  let exePath : FilePath := s!"./.lake/packages/{pkg}/.lake/build/bin/{exeFile}.exe"
  let exsits ← pathExists exePath
  if exsits then
    return exePath.toString
  return s!"lake exe {exeFile}"

/-- mk_exercise と mdgen と mdbook を順に実行し、
Lean ファイルから Markdown ファイルと HTML ファイルを生成する。-/
script build do

  -- `lake run mk_exercise` を使用すると遅くなってしまうのでコピペしている
  with_time running "mk_exercise"
    let cmd ← getBinary "mk-exercise" "mk_exercise"
    runCmd s!"{cmd} Examples/Solution Exercise"

  with_time running "mdgen"
    let cmd ← getBinary "mdgen" "mdgen"
    runCmd s!"{cmd} Examples src";
    runCmd s!"{cmd} Exercise src/Exercise"

  with_time running "mdbook"
    runCmd "mdbook build"

  return 0

end Script