From 2d3bec2209521d6f482a6fd9f52f39e9ccccfa6a Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 22 Aug 2021 11:17:18 -0400 Subject: [PATCH] feat: add proper CLI --- Lake.lean | 5 +- Lake/Cli.lean | 148 ++++++++++++++++++++++++++++--------- Lake/CliT.lean | 169 +++++++++++++++++++++++++++++++++++++++++++ Lake/Help.lean | 51 ++++++++----- Lake/LeanConfig.lean | 9 ++- Lake/Version.lean | 4 + 6 files changed, 325 insertions(+), 61 deletions(-) create mode 100644 Lake/CliT.lean diff --git a/Lake.lean b/Lake.lean index ecea28fb1a..f43d7a2371 100644 --- a/Lake.lean +++ b/Lake.lean @@ -11,9 +11,8 @@ import Lake.BuildTargets def main (args : List String) : IO UInt32 := do try Lake.setupLeanSearchPath - let (cmd, outerArgs, innerArgs) ← Lake.splitCmdlineArgs args - Lake.cli cmd outerArgs innerArgs + Lake.cli args pure 0 catch e => - IO.eprintln e -- avoid "uncaught exception: ..." + IO.eprintln <| "error: " ++ toString e -- avoid "uncaught exception: ..." pure 1 diff --git a/Lake/Cli.lean b/Lake/Cli.lean index 84dc50f6fe..2e89baf958 100644 --- a/Lake/Cli.lean +++ b/Lake/Cli.lean @@ -1,21 +1,18 @@ /- -Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone +Authors: Mac Malone -/ import Lake.Init import Lake.Help import Lake.BuildBin import Lake.LeanConfig +import Lake.CliT +open System namespace Lake -def getCwdPkg (args : List String) : IO Package := do - let pkg ← Package.fromDir "." args - if pkg.leanVersion ≠ leanVersionString then - IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ - leanVersionString ++ ", but package requires " ++ pkg.leanVersion ++ "\n" - return pkg +-- # Utilities def Package.run (script : String) (args : List String) (self : Package) : IO PUnit := if let some script := self.scripts.find? script then @@ -30,32 +27,113 @@ def removeDirAll (path : System.FilePath) : IO PUnit := do def Package.clean (self : Package) : IO PUnit := removeDirAll self.buildDir -def cli : (cmd : String) → (lakeArgs pkgArgs : List String) → IO Unit -| "new", [name], [] => new name -| "init", [name], [] => init name -| "run", [script], args => do (← getCwdPkg []).run script args -| "configure", [], pkgArgs => do configure (← getCwdPkg pkgArgs) -| "print-paths", imports, pkgArgs => do printPaths (← getCwdPkg pkgArgs) imports -| "build", [], pkgArgs => do build (← getCwdPkg pkgArgs) -| "build-lib", [], pkgArgs => do buildLib (← getCwdPkg pkgArgs) -| "build-bin", [], pkgArgs => do buildBin (← getCwdPkg pkgArgs) -| "clean", [], pkgArgs => do (← getCwdPkg pkgArgs).clean -| "help", [cmd], _ => IO.println <| help cmd -| "self-check", [], _ => verifyLeanVersion -| _, _, _ => throw <| IO.userError usage +-- # CLI -private def splitCmdlineArgsCore : List String → List String × List String -| [] => ([], []) -| (arg::args) => - if arg == "--" then - ([], args) - else - let (outerArgs, innerArgs) := splitCmdlineArgsCore args - (arg::outerArgs, innerArgs) +structure CliOptions where + wantsHelp : Bool := false + dir : FilePath := "." + file : FilePath := pkgFileName + subArgs : List String := [] -def splitCmdlineArgs : List String → IO (String × List String × List String) -| [] => throw <| IO.userError usage -| [cmd] => return (cmd, [], []) -| (cmd::rest) => - let (outerArgs, innerArgs) := splitCmdlineArgsCore rest - return (cmd, outerArgs, innerArgs) +abbrev CliM := CliT (StateT CliOptions IO) +-- abbrev LakeCliMethods := CliMethods (StateT CliState IO) + +namespace CliM +open CliT + +def getDir : CliM FilePath := + getThe CliOptions >>= (·.dir) + +def setDir (dir : FilePath) : CliM PUnit := + modifyThe CliOptions fun st => {st with dir := dir} + +def getFile : CliM FilePath := + getThe CliOptions >>= (·.file) + +def setFile (file : FilePath) : CliM PUnit := + modifyThe CliOptions fun st => {st with file := file} + +def getSubArgs : CliM (List String) := + getThe CliOptions >>= (·.subArgs) + +def setSubArgs (args : List String) : CliM PUnit := + modifyThe CliOptions fun st => {st with subArgs := args} + +def getWantsHelp : CliM Bool := + getThe CliOptions >>= (·.wantsHelp) + +def setWantsHelp : CliM PUnit := + modifyThe CliOptions fun st => {st with wantsHelp := true} + +def getPkg (args : List String) : CliM Package := do + let pkg ← Package.fromDir (← getDir) args (← getFile) + if pkg.leanVersion ≠ leanVersionString then + IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ + leanVersionString ++ ", but package requires " ++ pkg.leanVersion ++ "\n" + return pkg + +def takeArg : CliM String := do + match (← takeArg?) with + | none => throw <| IO.userError "missing argument" + | some arg => arg + +def takeFileArg : CliM FilePath := do + match (← takeArg?) with + | none => throw <| IO.userError "missing file argument" + | some arg => arg + +def unknownShortOption (opt : Char) : CliM PUnit := + throw <| IO.userError s!"unknown short option '-{opt}'" + +def shortOption : (opt : Char) → CliM PUnit +| 'h' => setWantsHelp +| 'd' => do setDir (← takeFileArg) +| 'f' => do setFile (← takeFileArg) +| opt => unknownShortOption opt + +def unknownLongOption (opt : String) : CliM PUnit := + throw <| IO.userError s!"unknown long option '{opt}'" + +def longOption : (opt : String) → CliM PUnit +| "--help" => setWantsHelp +| "--dir" => do setDir (← takeFileArg) +| "--file" => do setFile (← takeFileArg) +| "--" => do setSubArgs (← takeArgs) +| opt => unknownLongOption opt + +def command : (cmd : String) → CliM PUnit +| "new" => do new (← takeArg) +| "init" => do init (← takeArg) +| "run" => do (← getPkg []).run (← takeArg) (← getSubArgs) +| "configure" => do configure (← getPkg (← getSubArgs)) +| "print-paths" => do printPaths (← getPkg (← getSubArgs)) (← takeArgs) +| "build" => do build (← getPkg (← getSubArgs)) +| "build-lib" => do buildLib (← getPkg (← getSubArgs)) +| "build-bin" => do buildBin (← getPkg (← getSubArgs)) +| "clean" => do (← getPkg (← getSubArgs)).clean +| "help" => do IO.println <| help (← takeArg?) +| "self-check" => verifyLeanVersion +| cmd => throw <| IO.userError s!"unknown command '{cmd}'" + +def processArgs : CliM PUnit := do + match (← getArgs) with + | [] => throw <| IO.userError "expected command" + | ["--version"] => IO.println uiVersionString + | _ => -- normal CLI + processOptions + match (← takeArg?) with + | none => + if (← getWantsHelp) then IO.println usage else + throw <| IO.userError "expected command" + | some cmd => + let args ← collectArgs + if (← getWantsHelp) then IO.println (help cmd) else + command cmd + +def run (self : CliM PUnit) (args : List String) : IO PUnit := + CliT.run self args {shortOption, longOption, longShortOption := unknownLongOption} |>.run' {} + +end CliM + +def cli (args : List String) : IO PUnit := + CliM.processArgs.run args diff --git a/Lake/CliT.lean b/Lake/CliT.lean new file mode 100644 index 0000000000..f6a03aea25 --- /dev/null +++ b/Lake/CliT.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ + +namespace Lake + +-------------------------------------------------------------------------------- +-- # CLI Transformer Definition +-------------------------------------------------------------------------------- + +-- Involves trickery patterned after `MacroM` +-- to allow `BuildMethods` to refer to `BuildM` + +constant CliMethodsRefPointed : PointedType.{0} +def CliMethodsRef (m : Type → Type v) : Type := CliMethodsRefPointed.type + +abbrev CliT (m : Type → Type v) := + ReaderT (CliMethodsRef m) <| StateT (List String) m + +instance [Pure m] [Inhabited α] : Inhabited (CliT m α) := + ⟨fun _ _ => pure (Inhabited.default, Inhabited.default)⟩ + +structure CliMethods (m : Type → Type v) where + longOption : String → CliT m PUnit + longShortOption : String → CliT m PUnit + shortOption : Char → CliT m PUnit + +instance [Pure m] : Inhabited (CliMethods m) := + ⟨Inhabited.default, Inhabited.default, Inhabited.default⟩ + +namespace CliMethodsRef + +unsafe def mkImp (methods : CliMethods m) : CliMethodsRef m := + unsafeCast methods + +@[implementedBy mkImp] +constant mk (methods : CliMethods m) : CliMethodsRef m := + CliMethodsRefPointed.val + +instance : Coe (CliMethods m) (CliMethodsRef m) := ⟨mk⟩ +instance [Pure m] : Inhabited (CliMethodsRef m) := ⟨mk Inhabited.default⟩ + +unsafe def getImp [Pure m] (self : CliMethodsRef m) : CliMethods m := + unsafeCast self + +@[implementedBy getImp] +constant get [Pure m] (self : CliMethodsRef m) : CliMethods m + +end CliMethodsRef + +-------------------------------------------------------------------------------- +-- # CLI Utilities +-------------------------------------------------------------------------------- + +namespace CliT +variable [Monad m] + +/-- Run the CLI on the given argument list using the given methods. -/ +def run (self : CliT m α) (args : List String) (methods : CliMethods m) : m α := + ReaderT.run self methods |>.run' args + +/-- Get the remaining argument list. -/ +def getArgs : CliT m (List String) := + get + +/-- Replace the argument list. -/ +def setArgs (args : List String) : CliT m PUnit := + set args + +/-- Take the head of the remaining argument list (or none if empty). -/ +def takeArg? : CliT m (Option String) := + modifyGet fun | [] => (none, []) | arg :: args => (some arg, args) + +/-- Take the remaining argument list, leaving only an empty list. -/ +def takeArgs : CliT m (List String) := + modifyGet fun args => (args, []) + +/-- Add a string to the head of the remaining argument list. -/ +def consArg (arg : String) : CliT m PUnit := + modify fun args => arg :: args + +/-- Get the methods of this CLI. -/ +def getMethods : CliT m (CliMethods m) := + read >>= (·.get) + +/-- Change the methods of this CLI. -/ +def adaptMethods (f : CliMethods m → CliMethods m) (x : CliT m α) : CliT m α := + ReaderT.adapt (fun ref => CliMethodsRef.mk <| f ref.get) x + +/-- Process a short option (ex. `-x` or `--`). -/ +def shortOption (opt : Char) : CliT m PUnit := + getMethods >>= (·.shortOption opt) + +/-- Process a short option of the form `-x=arg`. -/ +def shortOptionEq (opt : String) : CliT m PUnit := do + consArg (opt.drop 3); shortOption opt[1] + +/-- Process a short option of the form `-xarg`. -/ +def shortOptionArg (opt : String) : CliT m PUnit := do + consArg (opt.drop 2); shortOption opt[1] + +/-- Process a short option of the form `"-x arg"`. -/ +def shortOptionSpace (opt : String) : CliT m PUnit := do + consArg <| opt.drop 2 |>.trimLeft; shortOption opt[1] + +/-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/ +def multiShortOption (opt : String) : CliT m PUnit := do + for i in [1:opt.length] do shortOption opt[i] + +/-- Process a long option (ex. `--long` or `"--long a1 a2"`). -/ +def longOption (opt : String) : CliT m PUnit := do + getMethods >>= (·.longOption opt) + +/-- Process a long short option (ex. `-long`, `-xarg`, `-xyz`). -/ +def longShortOption (opt : String) : CliT m PUnit := do + getMethods >>= (·.longShortOption opt) + +/-- + Process an option, short or long. + An option is an argument of length > 1 starting with a dash (`-`). + An option may consume additional elements of the argument list. +-/ +def option (opt : String) : CliT m PUnit := + if opt[1] == '-' then -- `--(.*)` + longOption opt + else + if opt.length == 2 then -- `-x` + shortOption opt[1] + else -- `-c(.+)` + match opt[2] with + | '=' => -- `-x=arg` + shortOptionEq opt + | ' ' => -- `"-x arg"` + shortOptionSpace opt + | _ => -- `-long` + longShortOption opt + +/-- Process the leading options of the remaining argument list. -/ +partial def processLeadingOptions : CliT m PUnit := do + match (← getArgs) with + | [] => pure () + | arg :: args => + let len := arg.length + if len > 1 && arg[0] == '-' then -- `-(.+)` + setArgs args + option arg + processLeadingOptions + else if len == 0 then -- skip empty leading args + setArgs args + processLeadingOptions + +/-- Process every option and collect the remaining arguments into the given `Array`. -/ +partial def collectArgsInto (arr : Array String) : CliT m (Array String) := do + processLeadingOptions + match (← takeArg?) with + | some arg => collectArgsInto (arr.push arg) + | none => arr + +/-- Process every option and collect the remaining arguments into an `Array`. -/ +def collectArgs : CliT m (Array String) := + collectArgsInto #[] + +/-- Process every option in the argument list. -/ +def processOptions : CliT m PUnit := do + setArgs (← collectArgs).toList + +end CliT diff --git a/Lake/Help.lean b/Lake/Help.lean index 452d72345e..c2295c8d26 100644 --- a/Lake/Help.lean +++ b/Lake/Help.lean @@ -9,26 +9,33 @@ import Lake.LeanVersion namespace Lake def usage := -s!"Lake version {versionString} (Lean version {uiLeanVersionString}) +uiVersionString ++ " -Usage: - lake +USAGE: + lake [OPTIONS] -new create a Lean package in a new directory -init create a Lean package in the current directory -run