Seasawher
commented
1 month ago 実行バイナリを .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
mk_exercise のリポジトリで lake run test を実行したとき：
lean-by-example のリポジトリで lake run build を実行したとき：
このように、２倍以上の時間がなぜかかかるようになってしまう…。なぜ？？？？
(mk_exercise のリポジトリにおけるパフォーマンステストには、lean-by-example のものと同じファイルを使用している）
Zulip: Omit compilation and run the executable binary in the .lake