Merge branch 'nightly'

Author: mhuisi

.github/workflows/check_nightly.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: checkout repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           ref: nightly
       - name: install elan

Cli/Basic.lean

@@ -18,6 +18,10 @@ def runExampleCmd (p : Parsed) : IO UInt32 := do
   let priority : Nat := p.flag! "priority" |>.as! Nat
   IO.println <| "Flag `--priority` always has at least a default value: " ++ toString priority
 
+  if p.hasFlag "module" then
+    let moduleName : ModuleName := p.flag! "module" |>.as! ModuleName
+    IO.println <| s!"Flag `--module` was set to `{moduleName}`."
+
   if let some setPathsFlag := p.flag? "set-paths" then
     IO.println <| toString <| setPathsFlag.as! (Array String)
   return 0
@@ -43,6 +47,9 @@ def exampleCmd : Cmd := `[Cli|
     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."
@@ -68,14 +75,15 @@ def exampleCmd : Cmd := `[Cli|
 def main (args : List String) : IO UInt32 :=
   exampleCmd.validate args
 
-#eval main <| "-i -o -p 1 --set-paths=path1,path2,path3 input output1 output2".splitOn " "
+#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
 /-
 Yields:
   Input: input
   Outputs: #[output1, output2]
   Flag `--invert` was set.
   Flag `--optimize` was set.
   Flag `--priority` always has at least a default value: 1
+  Flag `--module` was set to `Lean.Compiler`.
   #[path1, path2, path3]
 -/
 
@@ -121,6 +129,11 @@ Yields:
       -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.

Cli/Example.lean

@@ -1,5 +1,7 @@
 import Cli.Basic
 
+namespace Cli
+
 section Utils
   namespace Array
     /--
@@ -8,7 +10,7 @@ section Utils
     -/
     def leftUnionBy [Ord α] (key : β → α) (left : Array β) (right : Array β)
       : Array β := Id.run do
-      let leftMap := left.map (fun v => (key v, v)) |>.toList |> Std.RBMap.ofList (cmp := compare)
+      let leftMap := left.map (fun v => (key v, v)) |>.toList |> Lean.RBMap.ofList (cmp := compare)
       let mut result := left
       for v in right do
         if ¬ leftMap.contains (key v) then
@@ -21,7 +23,7 @@ section Utils
     -/
     def rightUnionBy [Ord α] (key : β → α) (left : Array β) (right : Array β)
       : Array β := Id.run do
-      let rightMap := right.map (fun v => (key v, v)) |>.toList |> Std.RBMap.ofList (cmp := compare)
+      let rightMap := right.map (fun v => (key v, v)) |>.toList |> Lean.RBMap.ofList (cmp := compare)
       let mut result := right
       for v in left.reverse do
         if ¬ rightMap.contains (key v) then
@@ -31,13 +33,11 @@ section Utils
     /-- Deletes all elements from `left` whose `key` is in `right`. -/
     def diffBy [Ord α] (key : β → α) (left : Array β) (right : Array α)
       : Array β :=
-      let rightMap := Std.RBTree.ofList (cmp := compare) right.toList
+      let rightMap := Lean.RBTree.ofList (cmp := compare) right.toList
       left.filter fun v => ¬ (rightMap.contains <| key v)
   end Array
 end Utils
 
-namespace Cli
-
 section Extensions
   /-- Prepends an author name to the description of the command. -/
   def author (author : String) : Extension := {
@@ -47,8 +47,8 @@ section Extensions
   /-- Appends a longer description to the end of the help. -/
   def longDescription (description : String) : Extension := {
       extend := fun cmd => cmd.update (furtherInformation? :=
-        some <| cmd.furtherInformation?.optStr ++ lines #[
-          cmd.furtherInformation?.optStr,
+        some <| Option.optStr cmd.furtherInformation? ++ lines #[
+          Option.optStr cmd.furtherInformation?,
           (if cmd.hasFurtherInformation then "\n" else "") ++ renderSection "DESCRIPTION" description
         ]
       )
@@ -58,7 +58,7 @@ section Extensions
   def helpSubCommand : Extension := {
       priority := 0
       extend   := fun cmd =>
-        let helpCmd := .mk 
+        let helpCmd := .mk
           (parent      := cmd)
           (name        := "help")
           (version?    := none)
@@ -67,7 +67,7 @@ section Extensions
         -- 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 
+        let helpCmd := helpCmd.update (run := fun _ => do
           cmd.toFullCmdWithoutExtensions.printHelp
           return 0)
         let subCmds := cmd.subCmds.set! (cmd.subCmds.size - 1) helpCmd
@@ -80,12 +80,12 @@ section Extensions
       if cmd.version?.isNone then
         panic! "Cli.versionSubCommand!: Cannot add `version` subcommand to command without a version."
       else
-        let helpCmd := .mk 
+        let helpCmd := .mk
           (parent      := cmd)
           (name        := "version")
           (version?    := none)
           (description := "Prints the version.")
-          (run         := fun _ => do 
+          (run         := fun _ => do
             cmd.toFullCmdWithoutExtensions.printVersion!
             return 0)
         cmd.update (subCmds := cmd.subCmds.push helpCmd)
@@ -111,7 +111,7 @@ section Extensions
         cmd.update (flags := newMetaFlags)
       postprocess := fun cmd parsed =>
         let defaultFlags := findDefaultFlags cmd
-        return { parsed with flags := parsed.flags.leftUnionBy (·.flag.longName) defaultFlags }
+        return { parsed with flags := Array.leftUnionBy (·.flag.longName) parsed.flags defaultFlags }
     }
 
   /--
@@ -134,7 +134,7 @@ section Extensions
         if parsed.hasFlag "help" ∨ parsed.hasFlag "version" then
           return parsed
         let requiredFlags := findRequiredFlags cmd
-        let missingFlags := requiredFlags.diffBy (·.longName) <| parsed.flags.map (·.flag.longName)
+        let missingFlags := Array.diffBy (·.longName) requiredFlags <| parsed.flags.map (·.flag.longName)
         if let some missingFlag ← pure <| missingFlags.get? 0 then
           throw s!"Missing required flag `--{missingFlag.longName}`."
         return parsed

Cli/Extensions.lean

@@ -388,4 +388,38 @@ section Info
     == "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
 
+section ModuleName
+  def ModuleName.parse? : String → Option ModuleName := ParseableType.parse?
+
+  section ValidInputs
+    #eval ModuleName.parse? "Lean.Mathlib.Data" == some `Lean.Mathlib.Data
+    #eval ModuleName.parse? "F00Bar.BarF00" == some `F00Bar.BarF00
+    #eval ModuleName.parse? "foo_bar" == some `foo_bar
+    #eval ModuleName.parse? "asdf.«foo bar»" == some `asdf.«foo bar»
+    #eval ModuleName.parse? "«1».«2»" == some `«1».«2»
+    #eval ModuleName.parse? "« »" == some `« »
+    #eval ModuleName.parse? "Lean/Mathlib/Data/Afile.lean" == some `Lean.Mathlib.Data.Afile
+    #eval ModuleName.parse? "Foo.lean" == some `Foo
+    #eval ModuleName.parse? "..lean" == some `«.»
+    #eval ModuleName.parse? " .lean" == some `« »
+    #eval ModuleName.parse? " /Foo.lean" == some `« ».Foo
+  end ValidInputs
+
+  section InvalidInputs
+    #eval ModuleName.parse? "" == none
+    #eval ModuleName.parse? "." == none
+    #eval ModuleName.parse? ".asdf" == none
+    #eval ModuleName.parse? "asdf." == none
+    #eval ModuleName.parse? "1.asdf" == none
+    #eval ModuleName.parse? "asdf.1" == none
+    #eval ModuleName.parse? "1asdf" == none
+    #eval ModuleName.parse? "foo bar" == none
+    #eval ModuleName.parse? "foo,bar" == none
+    #eval ModuleName.parse? "«»" == none
+    #eval ModuleName.parse? "x.«»" == none
+    #eval ModuleName.parse? ".lean" == none
+    #eval ModuleName.parse? "/foo.lean" == none
+  end InvalidInputs
+end ModuleName
+
 end Cli

Cli/Tests.lean

@@ -3,9 +3,9 @@
 See [the documentation of Lake](https://github.com/leanprover/lake).
 
 Use one of the following for the `<tag>` in the dependency source `Source.git "https://github.com/mhuisi/lean4-cli.git" "<tag>"`:
-- `main` if you want to stay in sync with Lean 4 milestone releases. The `main` branch will contain a working version of lean4-cli for the most recent Lean 4 milestone.
+- `main` if you want to stay in sync with Lean 4 stable releases. The `main` branch will contain a working version of lean4-cli for the most recent Lean 4 stable release.
 - `nightly` if you want to stay in sync with Lean 4 nightly releases. The `nightly` branch will contain a working version of lean4-cli for the most recent Lean 4 nightly build.
-- One of the specific release tags if you want to pin a specific version, e.g. `v1.0.0-lv4.0.0-m4` for v1.0.0 for the 4th Lean 4 milestone release or `v1.0.0-lnightly-2022-05-21` for v1.0.0 for the Lean 4 nightly version from 2022-05-21. Only nightlies where lean4-cli broke will receive a release tag.
+- One of the specific release tags if you want to pin a specific version, e.g. `v2.2.0-lv4.0.0` for v2.2.0 of lean4-cli and the Lean 4 stable release with version v4.0.0 or `v2.2.0-lnightly-2023-08-23` for v2.2.0 of lean4-cli and the Lean 4 nightly version from 2023-08-23.
 
 ### Configuration
 Commands are configured with a lightweight DSL. The following declarations define a command `exampleCmd` with two subcommands `installCmd` and `testCmd`. `runExampleCmd` denotes a handler that is called when the command is run and is described further down below in the **Command Handlers** subsection.
@@ -34,6 +34,9 @@ def exampleCmd : Cmd := `[Cli|
     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 be can 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."
@@ -77,6 +80,10 @@ def runExampleCmd (p : Parsed) : IO UInt32 := do
   let priority : Nat := p.flag! "priority" |>.as! Nat
   IO.println <| "Flag `--priority` always has at least a default value: " ++ toString priority
 
+  if p.hasFlag "module" then
+    let moduleName : ModuleName := p.flag! "module" |>.as! ModuleName
+    IO.println <| s!"Flag `--module` was set to `{moduleName}`."
+
   if let some setPathsFlag := p.flag? "set-paths" then
     IO.println <| toString <| setPathsFlag.as! (Array String)
   return 0
@@ -89,14 +96,15 @@ 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 --set-paths=path1,path2,path3 input output1 output2".splitOn " "
+#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
 /-
 Yields:
   Input: input
   Outputs: #[output1, output2]
   Flag `--invert` was set.
   Flag `--optimize` was set.
   Flag `--priority` always has at least a default value: 1
+  Flag `--module` was set to `Lean.Compiler`.
   #[path1, path2, path3]
 -/
 
@@ -143,6 +151,11 @@ FLAGS:
     -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.

README.md

@@ -3,5 +3,5 @@ open Lake DSL
 
 package Cli
 
-@[defaultTarget]
+@[default_target]
 lean_lib Cli

lakefile.lean

@@ -1 +1 @@
-leanprover/lean4:v4.0.0-m5
+leanprover/lean4:nightly-2023-08-23