From cfe4fbb927b542030470108add31c13f905cb9e4 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Thu, 23 Jul 2026 11:59:51 -0400
Subject: [PATCH] feat: support repeatable (accumulating) flags
---
Cli/Basic.lean | 28 +++++++++++++++----
CliTest/Example.lean | 64 +++++++++++++++++++++---------------------
CliTest/Tests.lean | 39 ++++++++++++++++++++++++++
README.md | 66 +++++++++++++++++++++++---------------------
4 files changed, 129 insertions(+), 68 deletions(-)
diff --git a/Cli/Basic.lean b/Cli/Basic.lean
index 2b1e254..c0cdc39 100644
--- a/Cli/Basic.lean
+++ b/Cli/Basic.lean
@@ -301,6 +301,9 @@ section Configuration
`Unit` is used to designate flags without a parameter.
-/
type : ParamType
+ /-- Whether the flag may be passed multiple times, accumulating its values.
+ Only meaningful for an `Array τ`-typed flag. -/
+ repeatable : Bool := false
deriving Inhabited, BEq, Repr
namespace Flag
@@ -1007,7 +1010,7 @@ section Macro
syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg
- syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
+ syntax flag := colGe literalIdent ("," literalIdent)? "..."? (" : " term)? "; " nameableStringArg
syntax "`[Cli|\n"
literalIdent runFun "; " ("[" nameableStringArg "]")?
@@ -1047,8 +1050,13 @@ section Macro
`(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type)
meta def expandFlag (flag : TSyntax `Cli.flag) : MacroM Term := do
- let `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) := flag
- | Macro.throwUnsupported
+ let (flagName1, flagName2, type, description, repeatable) ←
+ match flag with
+ | `(Cli.flag| $flagName1 $[, $flagName2]? ... $[ : $type]?; $description) =>
+ pure (flagName1, flagName2, type, description, true)
+ | `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) =>
+ pure (flagName1, flagName2, type, description, false)
+ | _ => Macro.throwUnsupported
let mut shortName := quote (none : Option String)
let mut longName := flagName1
if let some flagName2 := flagName2 then
@@ -1059,7 +1067,7 @@ section Macro
match type with
| none => unitType
| some type => type
- `(Flag.mk $shortName $(← expandLiteralIdent longName) $(← expandNameableStringArg description) $type)
+ `(Flag.mk $shortName $(← expandLiteralIdent longName) $(← expandNameableStringArg description) $type $(quote repeatable))
macro_rules
| `(`[Cli|
@@ -1155,7 +1163,10 @@ section Info
let columns : Array (String × String) := c.meta.flags.map fun flag =>
let shortName? : Option String := do return s!"-{← flag.shortName?}"
let names : String := optJoin #[optStr shortName?, s!"--{flag.longName}"] ", "
- let type? : Option String := if ¬ flag.isParamless then s!": {flag.type.name}" else none
+ let type? : Option String :=
+ if ¬ flag.isParamless then
+ (s!": {flag.type.name}" ++ (if flag.repeatable then " ..." else "") : String)
+ else none
(line #[names, optStr type?], flag.description)
renderTable "FLAGS" columns (emptyTablePlaceholder? := "None")
@@ -1336,6 +1347,11 @@ section Parsing
private def setParent (c? : Option Cmd) : ParseM Unit := do
set { ← get with parent? := c? }
private def pushParsedFlag (parsedFlag : Parsed.Flag) : ParseM Unit := do
+ if parsedFlag.flag.repeatable then
+ if let some i := (← parsedFlags).findIdx? (·.flag.longName = parsedFlag.flag.longName) then
+ let merged := { parsedFlag with value := (← parsedFlags)[i]!.value ++ "," ++ parsedFlag.value }
+ set { ← get with parsedFlags := (← parsedFlags).set! i merged }
+ return
set { ← get with parsedFlags := (← parsedFlags).push parsedFlag }
private def pushParsedPositionalArg (parsedPositionalArg : Parsed.Arg) : ParseM Unit := do
set { ← get with parsedPositionalArgs := (← parsedPositionalArgs).push parsedPositionalArg }
@@ -1380,6 +1396,8 @@ section Parsing
return none
private def ensureFlagUnique (flag : Flag) (inputFlag : InputFlag) : ParseM Unit := do
+ if flag.repeatable then
+ return
if (← parsedFlags).find? (·.flag.longName = flag.longName) |>.isSome then
throw <| ← parseError <| duplicateFlag flag inputFlag
diff --git a/CliTest/Example.lean b/CliTest/Example.lean
index af86a39..54a9b0d 100644
--- a/CliTest/Example.lean
+++ b/CliTest/Example.lean
@@ -42,17 +42,18 @@ def exampleCmd : Cmd := `[Cli|
"This string denotes the description of `exampleCmd`."
FLAGS:
- verbose; "Declares a flag `--verbose`. This is the description of the flag."
- i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
- o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
- p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
- that takes an argument of type `Nat`."
- module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
- which can be used to reference Lean modules like `Init.Data.Array` \
- or Lean files using a relative path like `Init/Data/Array.lean`."
- "set-paths" : Array String; "Declares a flag `--set-paths` \
- that takes an argument of type `Array Nat`. \
- Quotation marks allow the use of hyphens."
+ verbose; "Declares a flag `--verbose`. This is the description of the flag."
+ i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
+ o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
+ p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
+ that takes an argument of type `Nat`."
+ module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
+ which can be used to reference Lean modules like `Init.Data.Array` \
+ or Lean files using a relative path like `Init/Data/Array.lean`."
+ "set-paths" ... : Array String; "Declares a flag `--set-paths` \
+ that takes an argument of type `Array String`. \
+ The trailing `...` makes it repeatable: passing it \
+ multiple times accumulates the values."
ARGS:
input : String; "Declares a positional argument \
@@ -75,7 +76,7 @@ def exampleCmd : Cmd := `[Cli|
def main (args : List String) : IO UInt32 :=
exampleCmd.validate args
-#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
+#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1 --set-paths=path2,path3 input output1 output2".splitOn " "
/-
Yields:
Input: input
@@ -118,25 +119,26 @@ Yields:
exampleCmd [SUBCOMMAND] [FLAGS] ...
FLAGS:
- -h, --help Prints this message.
- --version Prints the version.
- --verbose Declares a flag `--verbose`. This is the
- description of the flag.
- -i, --invert Declares a flag `--invert` with an associated
- short alias `-i`.
- -o, --optimize Declares a flag `--optimize` with an associated
- short alias `-o`.
- -p, --priority : Nat Declares a flag `--priority` with an associated
- short alias `-p` that takes an argument of type
- `Nat`. [Default: `0`]
- --module : ModuleName Declares a flag `--module` that takes an
- argument of type `ModuleName` which can be used
- to reference Lean modules like `Init.Data.Array`
- or Lean files using a relative path like
- `Init/Data/Array.lean`.
- --set-paths : Array String Declares a flag `--set-paths` that takes an
- argument of type `Array Nat`. Quotation marks
- allow the use of hyphens.
+ -h, --help Prints this message.
+ --version Prints the version.
+ --verbose Declares a flag `--verbose`. This is the
+ description of the flag.
+ -i, --invert Declares a flag `--invert` with an
+ associated short alias `-i`.
+ -o, --optimize Declares a flag `--optimize` with an
+ associated short alias `-o`.
+ -p, --priority : Nat Declares a flag `--priority` with an
+ associated short alias `-p` that takes an
+ argument of type `Nat`. [Default: `0`]
+ --module : ModuleName Declares a flag `--module` that takes an
+ argument of type `ModuleName` which can be
+ used to reference Lean modules like
+ `Init.Data.Array` or Lean files using a
+ relative path like `Init/Data/Array.lean`.
+ --set-paths : Array String ... Declares a flag `--set-paths` that takes an
+ argument of type `Array String`. The
+ trailing `...` makes it repeatable: passing
+ it multiple times accumulates the values.
ARGS:
input : String Declares a positional argument that takes an
diff --git a/CliTest/Tests.lean b/CliTest/Tests.lean
index bfd41f0..351fc9f 100644
--- a/CliTest/Tests.lean
+++ b/CliTest/Tests.lean
@@ -94,6 +94,45 @@ def testCmd : Cmd := `[Cli|
require! #["typed1"]
]
+def testRepeatedCmd : Cmd := `[Cli|
+ repeatedcommand VIA doNothing;
+ "tests repeatable flags"
+
+ FLAGS:
+ t, tag ... : Array String; "a repeatable flag"
+ f, other; "a normal flag"
+]
+
+/--
+info: "cmd: repeatedcommand; flags: #[--tag=a]; positionalArgs: #[]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval testRepeatedCmd.processParsed "-t a"
+
+/--
+info: "repeatedcommand\ntests repeatable flags\n\nUSAGE:\n repeatedcommand [FLAGS]\n\nFLAGS:\n -h, --help Prints this message.\n -t, --tag : Array String ... a repeatable flag\n -f, --other a normal flag"
+-/
+#guard_msgs in
+#eval testRepeatedCmd.help
+
+/--
+info: "cmd: repeatedcommand; flags: #[--tag=a,b,c]; positionalArgs: #[]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval testRepeatedCmd.processParsed "-t a -t b -t c"
+
+/--
+info: "cmd: repeatedcommand; flags: #[--tag=a,b,c]; positionalArgs: #[]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval testRepeatedCmd.processParsed "-t a,b -t c"
+
+/--
+info: "cmd: repeatedcommand; flags: #[--tag=a,b, --other]; positionalArgs: #[]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval testRepeatedCmd.processParsed "-t a -f -t b"
+
section ValidInputs
/--
diff --git a/README.md b/README.md
index 099320f..ce3a6dd 100644
--- a/README.md
+++ b/README.md
@@ -26,17 +26,18 @@ def exampleCmd : Cmd := `[Cli|
"This string denotes the description of `exampleCmd`."
FLAGS:
- verbose; "Declares a flag `--verbose`. This is the description of the flag."
- i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
- o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
- p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
- that takes an argument of type `Nat`."
- module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
- which can be used to reference Lean modules like `Init.Data.Array` \
- or Lean files using a relative path like `Init/Data/Array.lean`."
- "set-paths" : Array String; "Declares a flag `--set-paths` \
- that takes an argument of type `Array Nat`. \
- Quotation marks allow the use of hyphens."
+ verbose; "Declares a flag `--verbose`. This is the description of the flag."
+ i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
+ o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
+ p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
+ that takes an argument of type `Nat`."
+ module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
+ which can be used to reference Lean modules like `Init.Data.Array` \
+ or Lean files using a relative path like `Init/Data/Array.lean`."
+ "set-paths" ... : Array String; "Declares a flag `--set-paths` \
+ that takes an argument of type `Array String`. \
+ The trailing `...` makes it repeatable: passing it \
+ multiple times accumulates the values."
ARGS:
input : String; "Declares a positional argument \
@@ -93,7 +94,7 @@ Below you can find some simple examples of how to pass user input to the Cli lib
def main (args : List String) : IO UInt32 :=
exampleCmd.validate args
-#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
+#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1 --set-paths=path2,path3 input output1 output2".splitOn " "
/-
Yields:
Input: input
@@ -137,25 +138,26 @@ USAGE:
exampleCmd [SUBCOMMAND] [FLAGS] ...
FLAGS:
- -h, --help Prints this message.
- --version Prints the version.
- --verbose Declares a flag `--verbose`. This is the
- description of the flag.
- -i, --invert Declares a flag `--invert` with an associated
- short alias `-i`.
- -o, --optimize Declares a flag `--optimize` with an associated
- short alias `-o`.
- -p, --priority : Nat Declares a flag `--priority` with an associated
- short alias `-p` that takes an argument of type
- `Nat`. [Default: `0`]
- --module : ModuleName Declares a flag `--module` that takes an
- argument of type `ModuleName` which can be used
- to reference Lean modules like `Init.Data.Array`
- or Lean files using a relative path like
- `Init/Data/Array.lean`.
- --set-paths : Array String Declares a flag `--set-paths` that takes an
- argument of type `Array String`. Quotation marks
- allow the use of hyphens.
+ -h, --help Prints this message.
+ --version Prints the version.
+ --verbose Declares a flag `--verbose`. This is the
+ description of the flag.
+ -i, --invert Declares a flag `--invert` with an
+ associated short alias `-i`.
+ -o, --optimize Declares a flag `--optimize` with an
+ associated short alias `-o`.
+ -p, --priority : Nat Declares a flag `--priority` with an
+ associated short alias `-p` that takes an
+ argument of type `Nat`. [Default: `0`]
+ --module : ModuleName Declares a flag `--module` that takes an
+ argument of type `ModuleName` which can be
+ used to reference Lean modules like
+ `Init.Data.Array` or Lean files using a
+ relative path like `Init/Data/Array.lean`.
+ --set-paths : Array String ... Declares a flag `--set-paths` that takes an
+ argument of type `Array String`. The
+ trailing `...` makes it repeatable: passing
+ it multiple times accumulates the values.
ARGS:
input : String Declares a positional argument that takes an
@@ -189,7 +191,7 @@ syntax positionalArg := colGe literalIdent " : " term "; " nameableStringArg
syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg
-syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
+syntax flag := colGe literalIdent ("," literalIdent)? "..."? (" : " term)? "; " nameableStringArg
syntax "`[Cli|\n"
literalIdent runFun "; " ("[" nameableStringArg "]")?