Lake script(run)でバイナリを実行する

Lakeでcargo runみたいなことをする方法をメモります。
試行錯誤過程混ざってます。

環境

$ lean --version
Lean (version 4.12.0, x86_64-unknown-linux-gnu, commit dc2533473114, Release)

lakefileはleanで書きます(型付けや補完がされるので)(Tomlではありません)。

本題

lake runとは

lake runはヘルプの通り、lake script runのエイリアスです。
lake scriptではscriptを実行できます。
scriptはlakefileのscript宣言で定義することができます(README)。

以下、公式に載ってる例です

import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

mainみたいな関数を定義していることがわかります。
あとここのdoc comment(?)は、lake script docで読めます。

外部コマンド呼び出し

次に外部コマンドを呼ぶ方法を探します。
leanprover-communityのgithub.ioのAPI documentで適当にProcessとかで調べると、IO.Process.SpawnArgsとか、IO.Process.spawnとかが出てきます。
外部コマンド呼び出しを他の言語でやったことある人ならなんとなく理解できると思います。

以下の例では標準出力と標準エラー出力を他のstreamみたいなものにしてそれをまたそのまま標準出力/標準エラー出力に流してます。(IO.Process.Stdio.toHandleTypeを使いました。)

processspawn.lean

let proc ← IO.Process.spawn
  ⟨{stdin := .inherit, stdout := .piped, stderr := .piped},
    ".lake/build/bin/foo", args.toArray, none, #[], false ⟩
IO.print (← proc.stdout.readToEnd)
IO.eprintln (← IO.FS.Handle.readToEnd proc.stderr)
let ret ← proc.wait

実行ファイルを自動で取得する

これで一応lake run fooみたいなのでバイナリターゲットを実行できるようになります(ビルドはできません)。
これはカッコ悪いし、何よりWindowsでは.exeがついてファイル名が変わるのでこの方法は使えません。

そこで、パッケージの定義的なものから実行ファイルを手に入れることにします。
バイナリパッケージ(ここでは仮にfooと呼びます)の型を見てみると、LeanExeConfigと出てきます。
先ほどと同じ感じでAPIを検索するとそれっぽいものLeanExeConfig.getがヒットしました。
そこから色々すると実行ファイルが取得できます。

まとめ

最終形はこんな感じです。

lakefile.lean

/--
Test binary target
-/
script test (args) do
  let exe := (← foo.get).file
  IO.println s!"exe: {exe}"
  IO.println s!"args: {args}"
  let proc ← IO.Process.spawn
    ⟨{stdin := .inherit, stdout := .piped, stderr := .piped},
      exe.toString, args.toArray, none, #[], false ⟩
  IO.print (← proc.stdout.readToEnd)
  IO.eprintln (← IO.FS.Handle.readToEnd proc.stderr)
  let ret ← proc.wait
  IO.println s!"returned: {ret}"
  pure ret

設定ファイルで型付けされたり補完が効く体験快適ですね^[1]。

脚注

1. Zennでシンタックスハイライトは効かないけど