LeanでCLIツールのバージョンを更新忘れしないようにしたい
２年くらい前に、Lean4でmdgenというCLIツールを作りました。この２年の間機能追加しながらメンテを続けているのですが、ひとつ困っていることがあります。
それは、CLIツールとしてのバージョン指定をチェックするのを忘れやすいということです。
前提としてLean4は毎月ペースで新しいリリースがあります。LTSなどというものはないので毎月更新しなければいけません。lean-updateというGitHub Actionを使って毎月自動で更新PRを出すのですが、Leanのバージョン指定ファイルであるlean-toolchainファイルの更新は自動化できるものの、CLIツールとしてのバージョンの文字列の更新は自動化できません。[1]
更新PRをレビューしているときの私は「ビルドとテストが通るかチェックすればいいよね」としか思っていないので、CLIバージョンの更新を忘れたままマージしてしまうことが多々あり、それに対する対策が必要だなと思いました。
上手くいかないアプローチ: Lean.versionString を使う
CLIバージョンの定義に Lean.versionString そのもの [2] を使うのはどうかと思いました。ちょうど以下のような感じです：
def versionString := s!"v{Lean.versionString}"
/-- API definition of `mdgen` command -/
def mkMdgenCmd : Cmd := `[Cli|
mdgen VIA runMdgenCmd; [versionString]
"mdgen is a tool to generate .md files from .lean files."
一見するとこれでうまくいくように見えます。しかし、実際にやってみたところこの方法は上手くいかないことがわかりました。この方法だと、mdgen リポジトリのバージョンではなくて、mdgen をインポートして使っている側のリポジトリの Lean バージョンが出力されてしまうようです。（……なぜ？という気持ちになりますが、実際そうだったので…）
テストスクリプトでチェックする
どうにかしてバージョン文字列を自動生成できないか悩んだ結果、いったん諦めて「バージョンが合っているかどうかを自動でチェックする」という方針に変えました。
つまり、mdgen リポジトリ内の lakefile に以下のように書いておきます：
def runCmdAux (input : String) : IO String := 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.println out.stderr
throw <| IO.userError s!"Failed to execute: {input}"
return out.stdout.trimRight
def checkVersion : IO Unit := do
let expectedVer := s!"v{Lean.versionString}"
let actualVer ← runCmdAux "lake exe mdgen --version"
if actualVer != expectedVer then
throw <| IO.userError s!"Version mismatch: expected {expectedVer}, got {actualVer}"
/-- run test by `lake test` -/
@[test_driver] script test do
checkVersion
return 0
これで、とりあえずmdgenのバージョン文字列を更新し忘れることはなくなるはずです。
おわりに
全部自動化するのは不可能ではないような気がするので挑戦してみたいです。
Discussion