boilerplate on `lakefile`

Stream: lean4

[Asei Inoue]

I always define the following runCmd function in my lakefile. It would be tedious to write this every time, but could it be written in short with only the built-ins provided?

see https://github.com/Seasawher/lean-book/blob/main/lakefile.lean

def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
  let out ← IO.Process.output {
    cmd := cmd
    args := args
  }
  let hasError := out.exitCode != 0
  if hasError then
    IO.eprint out.stderr
  return hasError

[Asei Inoue]

runCmd is useful for registering scripts in a lakefile, and I am borrowing it from yatima. (As I remember it).

[Asei Inoue]

see https://github.com/lurk-lab/yatima

[Asei Inoue]

It would be nice if there was an easy way to write bash in the lake file script.

[Asei Inoue]

Thank you for reading!