feat: add proper CLI
This commit is contained in:
tydeu
parent
1825e095e1
commit
2d3bec2209
6 changed files with 325 additions and 61 deletions
|
|
@ -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
|
||||
|
|
|
|||
148
Lake/Cli.lean
148
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
|
||||
|
|
|
|||
169
Lake/CliT.lean
Normal file
169
Lake/CliT.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -9,26 +9,33 @@ import Lake.LeanVersion
|
|||
namespace Lake
|
||||
|
||||
def usage :=
|
||||
s!"Lake version {versionString} (Lean version {uiLeanVersionString})
|
||||
uiVersionString ++ "
|
||||
|
||||
Usage:
|
||||
lake <command>
|
||||
USAGE:
|
||||
lake [OPTIONS] <COMMAND>
|
||||
|
||||
new <name> create a Lean package in a new directory
|
||||
init <name> create a Lean package in the current directory
|
||||
run <script> run arbitrary package scripts
|
||||
configure download and build dependencies
|
||||
build configure and build *.olean files
|
||||
build-lib configure and build a static library
|
||||
build-bin configure and build a native binary executable
|
||||
clean remove build outputs
|
||||
OPTIONS:
|
||||
--version print version and exit
|
||||
--help, -h print help of the program or a command and exit
|
||||
--dir, -d=file use the package configuration in a specific directory
|
||||
--file, -f=file use a specific file for the package configuration
|
||||
|
||||
COMMANDS:
|
||||
new <name> create a Lean package in a new directory
|
||||
init <name> create a Lean package in the current directory
|
||||
run <script> run arbitrary package scripts
|
||||
configure download and build dependencies
|
||||
build configure and build *.olean files
|
||||
build-lib configure and build a static library
|
||||
build-bin configure and build a native binary executable
|
||||
clean remove build outputs
|
||||
|
||||
See `lake help <command>` for more information on a specific command."
|
||||
|
||||
def helpNew :=
|
||||
"Create a Lean package in a new directory
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake new <name>
|
||||
|
||||
This command creates a new Lean package with the given name in
|
||||
|
|
@ -37,7 +44,7 @@ a new directory with the same name."
|
|||
def helpInit :=
|
||||
"Create a Lean package in the current directory
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake init <name>
|
||||
|
||||
This command creates a new Lean package with the given name in
|
||||
|
|
@ -46,7 +53,7 @@ the current directory."
|
|||
def helpRun :=
|
||||
"Run arbitrary package scripts
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake run <script> [-- <args>...]
|
||||
|
||||
This command runs the given script from the package configuration's
|
||||
|
|
@ -56,7 +63,7 @@ it will list the available scripts."
|
|||
def helpConfigure :=
|
||||
"Download and build dependencies
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake configure [-- <args>...]
|
||||
|
||||
This command sets up the directory with the package's dependencies
|
||||
|
|
@ -71,7 +78,7 @@ No copy is made of local dependencies."
|
|||
def helpBuild :=
|
||||
"Configure this package and build *.olean files
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake build [-- <args>...]
|
||||
|
||||
This command configures the package's dependencies and then builds the package
|
||||
|
|
@ -82,7 +89,7 @@ itself can be specified with `args`."
|
|||
def helpBuildLib :=
|
||||
"Configure this package and build a static library
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake build-lib [-- <args>...]
|
||||
|
||||
This command configures this package's dependencies, builds the package,
|
||||
|
|
@ -96,7 +103,7 @@ to the `Packager` itself can be specified with `args`."
|
|||
def helpBuildBin :=
|
||||
"Configure the package and build a native binary executable
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake build-bin [-- <args>...]
|
||||
|
||||
This command configures this package's dependencies, builds the package,
|
||||
|
|
@ -115,13 +122,13 @@ specified with `args`."
|
|||
def helpClean :=
|
||||
"Remove build outputs
|
||||
|
||||
Usage:
|
||||
USAGE:
|
||||
lake clean [-- <args>...]
|
||||
|
||||
Deletes the build directory of the package.
|
||||
Arguments to the `Packager` itself can be specified with `args`."
|
||||
|
||||
def help : (cmd : String) → String
|
||||
def helpCmd : (cmd : String) → String
|
||||
| "new" => helpNew
|
||||
| "init" => helpInit
|
||||
| "run" => helpRun
|
||||
|
|
@ -131,3 +138,7 @@ def help : (cmd : String) → String
|
|||
| "build-bin" => helpBuildBin
|
||||
| "clean" => helpClean
|
||||
| _ => usage
|
||||
|
||||
def help : (cmd? : Option String) → String
|
||||
| some cmd => helpCmd cmd
|
||||
| none => usage
|
||||
|
|
|
|||
|
|
@ -36,9 +36,12 @@ unsafe def fromLeanFileUnsafe
|
|||
else
|
||||
throw <| IO.userError <| s!"package configuration (at {path}) has errors"
|
||||
|
||||
@[implementedBy fromLeanFileUnsafe]
|
||||
constant fromLeanFile (path : FilePath) (root : FilePath) (args : List String := []) : IO Package
|
||||
|
||||
unsafe def fromDirUnsafe
|
||||
(path : FilePath) (args : List String := []) : IO Package :=
|
||||
fromLeanFileUnsafe (path / pkgFileName) path args
|
||||
(dir : FilePath) (args : List String := []) (file := pkgFileName) : IO Package :=
|
||||
fromLeanFileUnsafe (dir / file) dir args
|
||||
|
||||
@[implementedBy fromDirUnsafe]
|
||||
constant fromDir (path : FilePath) (args : List String := []) : IO Package
|
||||
constant fromDir (dir : FilePath) (args : List String := []) (file := pkgFileName) : IO Package
|
||||
|
|
|
|||
|
|
@ -3,9 +3,13 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.LeanVersion
|
||||
|
||||
namespace Lake
|
||||
|
||||
def version.major := 2
|
||||
def version.minor := 0
|
||||
def version.isPre := true
|
||||
def versionString := s!"{version.major}.{version.minor}-pre"
|
||||
def uiVersionString :=
|
||||
s!"Lake version {versionString} (Lean version {uiLeanVersionString})"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue