chore: resolve conflicts & update toolchain version to m5

Cli/Example.lean

@@ -2,9 +2,6 @@ import Cli
 
 open Cli
 
-def doNothing (p : Parsed) : IO UInt32 :=
-  return 0
-
 def runExampleCmd (p : Parsed) : IO UInt32 := do
   let input   : String       := p.positionalArg! "input" |>.as! String
   let outputs : Array String := p.variableArgsAs! String
@@ -26,13 +23,14 @@ def runExampleCmd (p : Parsed) : IO UInt32 := do
   return 0
 
 def installCmd := `[Cli|
-  installCmd VIA doNothing; ["0.0.1"]
-  "installCmd provides an example for a subcommand without flags or arguments."
+  installCmd NOOP;
+  "installCmd provides an example for a subcommand without flags or arguments that does nothing. " ++
+  "Versions can be omitted."
 ]
 
 def testCmd := `[Cli|
-  testCmd VIA doNothing; ["0.0.1"]
-  "testCmd provides another example for a subcommand without flags or arguments."
+  testCmd NOOP;
+  "testCmd provides another example for a subcommand without flags or arguments that does nothing."
 ]
 
 def exampleCmd : Cmd := `[Cli|
@@ -135,7 +133,7 @@ Yields:
 
   SUBCOMMANDS:
       installCmd  installCmd provides an example for a subcommand without flags or
-                  arguments.
+                  arguments that does nothing. Versions can be omitted.
       testCmd     testCmd provides another example for a subcommand without flags
-                  or arguments.
+                  or arguments that does nothing.
 -/

Cli/Extensions.lean

@@ -41,39 +41,76 @@ namespace Cli
 section Extensions
   /-- Prepends an author name to the description of the command. -/
   def author (author : String) : Extension := {
-      extendMeta := fun meta => { meta with description := s!"{author}\n{meta.description}" }
+      extend := fun cmd => cmd.update (description := s!"{author}\n{cmd.description}")
     }
 
   /-- Appends a longer description to the end of the help. -/
   def longDescription (description : String) : Extension := {
-      extendMeta := fun meta => { meta with furtherInformation? :=
-        some <| meta.furtherInformation?.optStr ++ lines #[
-          meta.furtherInformation?.optStr,
-          (if meta.furtherInformation?.isSome then "\n" else "") ++ renderSection "DESCRIPTION" description
+      extend := fun cmd => cmd.update (furtherInformation? :=
+        some <| cmd.furtherInformation?.optStr ++ lines #[
+          cmd.furtherInformation?.optStr,
+          (if cmd.hasFurtherInformation then "\n" else "") ++ renderSection "DESCRIPTION" description
         ]
-      }
+      )
     }
 
+  /-- Adds a `help` subcommand. -/
+  def helpSubCommand : Extension := {
+      priority := 0
+      extend   := fun cmd =>
+        let helpCmd := .mk 
+          (parent      := cmd)
+          (name        := "help")
+          (version?    := none)
+          (description := "Prints this message.")
+          (run         := fun _ => pure 0)
+        -- adding it once without a command handler ensures that the help will include
+        -- the help subcommand itself
+        let cmd := cmd.update (subCmds := cmd.subCmds.push helpCmd)
+        let helpCmd := helpCmd.update (run := fun _ => do 
+          cmd.toFullCmdWithoutExtensions.printHelp
+          return 0)
+        let subCmds := cmd.subCmds.set! (cmd.subCmds.size - 1) helpCmd
+        cmd.update (subCmds := subCmds)
+    }
+
+  /-- Adds a `version` subcommand. -/
+  def versionSubCommand! : Extension := {
+    extend := fun cmd =>
+      if cmd.version?.isNone then
+        panic! "Cli.versionSubCommand!: Cannot add `version` subcommand to command without a version."
+      else
+        let helpCmd := .mk 
+          (parent      := cmd)
+          (name        := "version")
+          (version?    := none)
+          (description := "Prints the version.")
+          (run         := fun _ => do 
+            cmd.toFullCmdWithoutExtensions.printVersion!
+            return 0)
+        cmd.update (subCmds := cmd.subCmds.push helpCmd)
+  }
+
   /--
   Sets default values for flags that were not set by the user according to
   `defaults := #[(long flag name, default value), ...]` and denotes the default value
   in the flag description of the help.
   Panics if one of the designated long flag names cannot be found in the command.
   -/
   def defaultValues! (defaults : Array (String × String)) : Extension :=
-    let findDefaultFlags meta := defaults.map <| fun (longName, defaultValue) =>
-      ⟨meta.flag! longName, defaultValue⟩
+    let findDefaultFlags cmd := defaults.map <| fun (longName, defaultValue) =>
+      ⟨cmd.flag! longName, defaultValue⟩
     {
-      extendMeta := fun meta =>
-        let defaultFlags := findDefaultFlags meta
-        let newMetaFlags := meta.flags.map fun flag =>
+      extend := fun cmd =>
+        let defaultFlags := findDefaultFlags cmd
+        let newMetaFlags := cmd.flags.map fun flag =>
           if let some defaultFlag := defaultFlags.find? (·.flag.longName = flag.longName) then
             { flag with description := flag.description ++ s!" [Default: `{defaultFlag.value}`]" }
           else
             flag
-        { meta with flags := newMetaFlags }
-      postprocess := fun meta parsed =>
-        let defaultFlags := findDefaultFlags meta
+        cmd.update (flags := newMetaFlags)
+      postprocess := fun cmd parsed =>
+        let defaultFlags := findDefaultFlags cmd
         return { parsed with flags := parsed.flags.leftUnionBy (·.flag.longName) defaultFlags }
     }
 
@@ -83,20 +120,20 @@ section Extensions
   Panics if one of the designated long flag names cannot be found in the command.
   -/
   def require! (requiredFlags : Array String) : Extension :=
-    let findRequiredFlags meta := requiredFlags.map (meta.flag! ·)
+    let findRequiredFlags cmd := requiredFlags.map (cmd.flag! ·)
     {
-      extendMeta := fun meta =>
-        let requiredFlags := findRequiredFlags meta
-        let newMetaFlags := meta.flags.map fun flag =>
-          if let some requiredFlag := requiredFlags.find? (·.longName = flag.longName) then
+      extend := fun cmd =>
+        let requiredFlags := findRequiredFlags cmd
+        let newMetaFlags := cmd.flags.map fun flag =>
+          if requiredFlags.find? (·.longName = flag.longName) |>.isSome then
             { flag with description := "[Required] " ++ flag.description }
           else
             flag
-        { meta with flags := newMetaFlags }
-      postprocess := fun meta parsed => do
+        cmd.update (flags := newMetaFlags)
+      postprocess := fun cmd parsed => do
         if parsed.hasFlag "help" ∨ parsed.hasFlag "version" then
           return parsed
-        let requiredFlags := findRequiredFlags meta
+        let requiredFlags := findRequiredFlags cmd
         let missingFlags := requiredFlags.diffBy (·.longName) <| parsed.flags.map (·.flag.longName)
         if let some missingFlag ← pure <| missingFlags.get? 0 then
           throw s!"Missing required flag `--{missingFlag.longName}`."

Cli/Tests.lean

@@ -12,29 +12,33 @@ section Utils
 
   instance [Repr α] [Repr β] : Repr (Except α β) where
     reprPrec
-    | Except.ok a,    n => s!"Except.ok ({repr a})"
-    | Except.error b, n => s!"Except.error ({repr b})"
+    | Except.ok a,    _ => s!"Except.ok ({repr a})"
+    | Except.error b, _ => s!"Except.error ({repr b})"
 
   def Cmd.processParsed (c : Cmd) (args : String) : String := Id.run do
     let mut args := args.splitOn
     if args = [""] then
       args := []
     match c.process args with
-    | Except.ok (cmd, parsed) =>
+    | Except.ok (_, parsed) =>
       return toString parsed
-    | Except.error (cmd, error) =>
+    | Except.error (_, error) =>
       return error
+
+  def Cmd.extendedHelp (c : Cmd) : String :=
+    c.extension!.extend (.ofFullCmd c) |>.toFullCmd c |>.help
+
 end Utils
 
-def doNothing (p : Parsed) : IO UInt32 := return 0
+def doNothing (_ : Parsed) : IO UInt32 := return 0
 
 def testSubSubCmd : Cmd := `[Cli|
-  testsubsubcommand VIA doNothing; ["0.0.2"]
+  testsubsubcommand VIA doNothing;
   "does this even do anything?"
 ]
 
 def testSubCmd1 : Cmd := `[Cli|
-  testsubcommand1 VIA doNothing; ["0.0.1"]
+  testsubcommand1 NOOP; ["0.0.1"]
   "a properly short description"
 
   FLAGS:
@@ -45,6 +49,10 @@ def testSubCmd1 : Cmd := `[Cli|
 
   SUBCOMMANDS:
     testSubSubCmd
+
+  EXTENSIONS:
+    helpSubCommand;
+    versionSubCommand!
 ]
 
 def testSubCmd2 : Cmd := `[Cli|
@@ -134,8 +142,17 @@ section ValidInputs
     (testCmd.processParsed "testsubcommand1 testsubsubcommand")
     == "cmd: testcommand testsubcommand1 testsubsubcommand; flags: #[]; positionalArgs: #[]; variableArgs: #[]"
 
-  #eval (testCmd.processParsed "testsubcommand2 --run asdf,geh")
+  #eval 
+    (testCmd.processParsed "testsubcommand2 --run asdf,geh")
     == "cmd: testcommand testsubcommand2; flags: #[--run]; positionalArgs: #[<ominous-input=asdf,geh>]; variableArgs: #[]"
+
+  #eval 
+    (testCmd.processParsed "testsubcommand1 help")
+    == "cmd: testcommand testsubcommand1 help; flags: #[]; positionalArgs: #[]; variableArgs: #[]"
+
+  #eval 
+    (testCmd.processParsed "testsubcommand1 version")
+    == "cmd: testcommand testsubcommand1 version; flags: #[]; positionalArgs: #[]; variableArgs: #[]"
 end ValidInputs
 
 section InvalidInputs
@@ -242,7 +259,7 @@ section Info
     == "testcommand [0.0.0]\nsome short description that happens to be much longer than necessary and hence\nneeds to be wrapped to fit into an 80 character width limit\n\nUSAGE:\n    testcommand [SUBCOMMAND] [FLAGS] <input1> <input2> <outputs>...\n\nFLAGS:\n    -h, --help                 Prints this message.\n    --version                  Prints the version.\n    --verbose                  a very verbose flag description that also needs\n                               to be wrapped to fit into an 80 character width\n                               limit\n    -x, --unknown1             this flag has a short name\n    -xn, --unknown2            short names do not need to be prefix-free\n    -ny, --unknown3            -xny will parse as -x -ny and not fail to parse\n                               as -xn -y\n    -t, --typed1 : String      flags can have typed parameters\n    -ty, --typed2              -ty parsed as --typed2, not -t=y\n    -p-n, --level-param : Nat  hyphens work, too\n\nARGS:\n    input1 : String     another very verbose description that also needs to be\n                        wrapped to fit into an 80 character width limit\n    input2 : Array Nat  arrays!\n    outputs : Nat       varargs!\n\nSUBCOMMANDS:\n    testsubcommand1  a properly short description\n    testsubcommand2  does not do anything interesting"
 
   #eval
-    testCmd.version
+    testCmd.meta.version!
     == "0.0.0"
 
   /-
@@ -294,19 +311,18 @@ section Info
     == "testcommand testsubcommand2 [0.0.-1]\ndoes not do anything interesting\n\nUSAGE:\n    testcommand testsubcommand2 [FLAGS] <ominous-input>\n\nFLAGS:\n    -h, --help  Prints this message.\n    --version   Prints the version.\n    -r, --run   really, this does not do anything. trust me.\n\nARGS:\n    ominous-input : Array String  what could this be for?"
 
   /-
-  testcommand testsubcommand1 testsubsubcommand [0.0.2]
+  testcommand testsubcommand1 testsubsubcommand
   does this even do anything?
 
   USAGE:
       testcommand testsubcommand1 testsubsubcommand [FLAGS]
 
   FLAGS:
       -h, --help  Prints this message.
-      --version   Prints the version.
   -/
   #eval
     (testCmd.subCmd! "testsubcommand1" |>.subCmd! "testsubsubcommand").help
-    == "testcommand testsubcommand1 testsubsubcommand [0.0.2]\ndoes this even do anything?\n\nUSAGE:\n    testcommand testsubcommand1 testsubsubcommand [FLAGS]\n\nFLAGS:\n    -h, --help  Prints this message.\n    --version   Prints the version."
+    == "testcommand testsubcommand1 testsubsubcommand\ndoes this even do anything?\n\nUSAGE:\n    testcommand testsubcommand1 testsubsubcommand [FLAGS]\n\nFLAGS:\n    -h, --help  Prints this message."
 
   /-
   testcommand [0.0.0]
@@ -344,9 +360,32 @@ section Info
   DESCRIPTION:
       this could be really long, but i'm too lazy to type it out.
   -/
-  #eval
-    (testCmd.update' (meta := testCmd.extension!.extendMeta testCmd.meta)).help
+  #eval testCmd.extendedHelp
     == "testcommand [0.0.0]\nmhuisi\nsome short description that happens to be much longer than necessary and hence\nneeds to be wrapped to fit into an 80 character width limit\n\nUSAGE:\n    testcommand [SUBCOMMAND] [FLAGS] <input1> <input2> <outputs>...\n\nFLAGS:\n    -h, --help                 Prints this message.\n    --version                  Prints the version.\n    --verbose                  a very verbose flag description that also needs\n                               to be wrapped to fit into an 80 character width\n                               limit\n    -x, --unknown1             this flag has a short name\n    -xn, --unknown2            short names do not need to be prefix-free\n    -ny, --unknown3            -xny will parse as -x -ny and not fail to parse\n                               as -xn -y\n    -t, --typed1 : String      [Required] flags can have typed parameters\n    -ty, --typed2              -ty parsed as --typed2, not -t=y\n    -p-n, --level-param : Nat  hyphens work, too [Default: `0`]\n\nARGS:\n    input1 : String     another very verbose description that also needs to be\n                        wrapped to fit into an 80 character width limit\n    input2 : Array Nat  arrays!\n    outputs : Nat       varargs!\n\nSUBCOMMANDS:\n    testsubcommand1  a properly short description\n    testsubcommand2  does not do anything interesting\n\nDESCRIPTION:\n    this could be really long, but i'm too lazy to type it out."
+
+  /-
+  testsubcommand1 [0.0.1]
+  a properly short description
+
+  USAGE:
+      testsubcommand1 [SUBCOMMAND] [FLAGS] <city-location>
+
+  FLAGS:
+      -h, --help          Prints this message.
+      --version           Prints the version.
+      --launch-the-nukes  please avoid passing this flag at all costs.
+                          if you like, you can have newlines in descriptions.
+
+  ARGS:
+      city-location : String  can also use hyphens
+
+  SUBCOMMANDS:
+      testsubsubcommand  does this even do anything?
+      version            Prints the version.
+      help               Prints this message.
+  -/
+  #eval testSubCmd1.extendedHelp
+    == "testsubcommand1 [0.0.1]\na properly short description\n\nUSAGE:\n    testsubcommand1 [SUBCOMMAND] [FLAGS] <city-location>\n\nFLAGS:\n    -h, --help          Prints this message.\n    --version           Prints the version.\n    --launch-the-nukes  please avoid passing this flag at all costs.\n                        if you like, you can have newlines in descriptions.\n\nARGS:\n    city-location : String  can also use hyphens\n\nSUBCOMMANDS:\n    testsubsubcommand  does this even do anything?\n    version            Prints the version.\n    help               Prints this message."
 end Info
 
 end Cli