From 3e9cbb049e3fd96b9b3250667c30005384cf3714 Mon Sep 17 00:00:00 2001 From: qwjyh Date: Mon, 3 Jun 2024 13:13:33 +0900 Subject: [PATCH] init --- .gitignore | 1 + Lean4CliExample.lean | 4 ++ Lean4CliExample/Basic.lean | 1 + Lean4CliExample/Cli.lean | 80 ++++++++++++++++++++++++++++++++++++++ Main.lean | 13 +++++++ README.md | 2 + lake-manifest.json | 14 +++++++ lakefile.lean | 14 +++++++ lean-toolchain | 1 + 9 files changed, 130 insertions(+) create mode 100644 .gitignore create mode 100644 Lean4CliExample.lean create mode 100644 Lean4CliExample/Basic.lean create mode 100644 Lean4CliExample/Cli.lean create mode 100644 Main.lean create mode 100644 README.md create mode 100644 lake-manifest.json create mode 100644 lakefile.lean create mode 100644 lean-toolchain diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/Lean4CliExample.lean b/Lean4CliExample.lean new file mode 100644 index 0000000..31642b4 --- /dev/null +++ b/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 diff --git a/Lean4CliExample/Basic.lean b/Lean4CliExample/Basic.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/Lean4CliExample/Basic.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/Lean4CliExample/Cli.lean b/Lean4CliExample/Cli.lean new file mode 100644 index 0000000..558a768 --- /dev/null +++ b/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 " ++ + "that takes an argument of type `String`." + ...outputs : String; "Declares a variable argument ... " ++ + "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")] +] + diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..885b6d6 --- /dev/null +++ b/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 " " diff --git a/README.md b/README.md new file mode 100644 index 0000000..d774751 --- /dev/null +++ b/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). diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..1e3525b --- /dev/null +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..7a976e6 --- /dev/null +++ b/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 diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..2bf5ad0 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +stable