Lake script flag "passthrough"?

Stream: lean4

[Rish Vaishnav]

When running a lake script, is there a way to instruct the CLI interpreter to "pass through" some flags to the script's argument list, without them being interpreted as flags to lake itself? For example, if I have the following lakefile.lean, with the script test that runs a Lean-generated executable with arguments passed down from the command line:

import Lake
open Lake DSL

require Cli from git
  "https://github.com/leanprover/lean4-cli" @ "main"

package «ex» where
  -- add package configuration options here

@[default_target]
lean_exe «ex» where
  root := `Main
  supportInterpreter := true

def runCmd (cmd : String) : ScriptM $ IO.Process.Output := do
  let cmd := cmd.splitOn " "
  if h : cmd ≠ [] then
    let (cmd, args) := match h' : cmd with
      | cmd :: args => (cmd, ⟨args⟩)
      | []          => absurd h' (h' ▸ h)
    IO.Process.output {
      cmd  := cmd
      args := args
    }
  else pure {exitCode := 0, stdout := "", stderr := ""}

def argsString (args : List String) :=
  args.foldl (init := "") fun acc arg => acc ++ " " ++ arg

script test (args) do
  IO.println s!"running test script {args}..."
  let {exitCode, stdout, stderr} ← runCmd s!"lake exe ex{argsString args}"
  IO.println stderr
  IO.println stdout
  pure exitCode

with Main.lean:

import Cli
open Cli

def runExCmd (p : Parsed) : IO UInt32 := do
  if p.hasFlag "ex" then
    IO.println "Example flag was set."

  return 0

def exCmd : Cmd := `[Cli|
  exCmd VIA runExCmd; ["0.0.1"]
  "Example."

  FLAGS:
    x, ex;      "example flag"
]

def main (args : List String) : IO UInt32 :=
  exCmd.validate args

I will get this error if I try to pass in the flag:

$ lake run test -x
error: unknown short option '-x'

lake run test '-x' gives the same error and lake run test -- -x seems to just ignore the flag. Could it be possible to pass down flags like this, or should I just make a different script for every flag combination that I need?

[Mac Malone]

Oops! This is a bug! lean4#3064 will fix this (and test it to make sure this bug doesn't happen again).

[Rish Vaishnav]

Great, thank you for the quick fix!