init

.gitignore

@@ -0,0 +1 @@
+/.lake

Lean4CliExample.lean

@@ -0,0 +1,4 @@
+-- This module serves as the root of the `Lean4CliExample` library.
+-- Import modules here that should be built as part of the library.
+import «Lean4CliExample».Basic
+import «Lean4CliExample».Cli

Lean4CliExample/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

Lean4CliExample/Cli.lean

@@ -0,0 +1,80 @@
+import Cli
+
+def name := "hoge"
+
+open Cli
+
+/---
+Handler
+--/
+def runExampleCmd (p : Parsed) : IO UInt32 := do
+  let input : String := p.positionalArg! "input" |>.as! String
+  let outputs : Array String := p.variableArgsAs! String
+  IO.println <| "Input: " ++ input
+  IO.println <| "outputs: " ++ toString outputs
+
+  if p.hasFlag "verbose" then
+    IO.println "Flag `--verbose` was set."
+  if p.hasFlag "invert" then
+    IO.println "Flag `--invert` was set."
+  if p.hasFlag "optimize" then
+    IO.println "Flag `--optimize` was set."
+
+  let priority : _ := 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 : _ := 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
+
+def installCmd := `[Cli|
+  installCmd NOOP;
+  "installCmd provides an example for a subcommand without flags or arguments that does nothing. " ++
+  "Versions can be omitted."
+]
+
+def testCmd := `[Cli|
+  testCmd NOOP;
+  "testCmd provides another example for a subcommand without flags or arguments that does 
+  nothing."
+]
+
+def exampleCmd : Cmd := `[Cli|
+  exampleCmd VIA runExampleCmd; ["0.0.1"]
+  "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 or 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."
+
+  ARGS:
+    input : String;       "Declares a positional argument <input> " ++
+                          "that takes an argument of type `String`."
+    ...outputs : String;  "Declares a variable argument <output>... " ++
+                          "that takes an arbitrary amount of arguments of type `String`."
+
+  SUBCOMMANDS:
+    installCmd;
+    testCmd
+
+  -- The EXTENSIONS section denotes features that were added as an external extension to the library.
+  -- `./Cli/Extensions.lean` provides some commonly useful examples.
+  EXTENSIONS:
+    author "qwjyh";
+    defaultValues! #[("priority", "0")]
+]
+

Main.lean

@@ -0,0 +1,13 @@
+import «Lean4CliExample»
+
+/---
+Main entry
+--/
+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 <| "-io -p1 input".splitOn " "
+
+#eval main <| "--version".splitOn " "

README.md

@@ -0,0 +1,2 @@
+# Lean4 Cli Example
+Trying [lean4-cli](https://github.com/leanprover/lean4-cli) which I found [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Command.20line.20argument.20parsing).

lake-manifest.json

@@ -0,0 +1,14 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "lean4_cli_example",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,14 @@
+import Lake
+open Lake DSL
+
+package «lean4_cli_example» where
+  -- add package configuration options here
+
+require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
+
+lean_lib «Lean4CliExample» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «lean4_cli_example» where
+  root := `Main

lean-toolchain

@@ -0,0 +1 @@
+stable