max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: lake: add upgrade and exec CLI aliases

Browse source
This commit is contained in:
tydeu 2023-09-11 19:25:23 -04:00 • committed by Mac Malone
parent 5983abcf78
commit 0bb6bcf24c
2 changed files with 42 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/lake/Lake/CLI/Help.lean
View file

@ -111,6 +111,8 @@ def helpUpdate :=
USAGE:
lake update [<package>...]
ALIAS: lake upgrade
Updates the Lake package manifest (i.e., `lake-manifest.json`),
downloading and upgrading packages as needed. For each new (transitive) git
dependency, the appropriate commit is cloned into a subdirectory of
@ -160,6 +162,8 @@ def helpScriptList :=
USAGE:
lake script list
ALIAS: lake scripts
This command prints the list of all available scripts in the workspace."
def helpScriptRun :=
@ -168,6 +172,8 @@ def helpScriptRun :=
USAGE:
lake script run [[<package>/]<script>] [<args>...]
ALIAS: lake run
This command runs the `script` of the workspace (or the specific `package`),
passing `args` to it.
@ -225,28 +231,30 @@ def helpExe :=
USAGE:
lake exe <exe-target> [<args>...]
ALIAS: lake exec
Looks for the executable target in the workspace (see `lake help build` to
learn how to specify targets), builds it if it is out of date, and then runs
it with the given `args` in Lake's environment (see `lake help env` for how
the environment is set up)."
def helpScript : (cmd : String) → String
| "list" => helpScriptList
| "run" => helpScriptRun
| "doc" => helpScriptDoc
| _ => helpScriptCli
| "list" => helpScriptList
| "run" => helpScriptRun
| "doc" => helpScriptDoc
| _ => helpScriptCli
def help : (cmd : String) → String
| "new" => helpNew
| "init" => helpInit
| "build" => helpBuild
| "update" => helpUpdate
| "upload" => helpUpload
| "clean" => helpClean
| "script" => helpScriptCli
| "scripts" => helpScriptList
| "run" => helpScriptRun
| "serve" => helpServe
| "env" => helpEnv
| "exe" => helpExe
| _ => usage
| "new" => helpNew
| "init" => helpInit
| "build" => helpBuild
| "update" | "upgrade" => helpUpdate
| "upload" => helpUpload
| "clean" => helpClean
| "script" => helpScriptCli
| "scripts" => helpScriptList
| "run" => helpScriptRun
| "serve" => helpServe
| "env" => helpEnv
| "exe" | "exec" => helpExe
| _ => usage

34
src/lake/Lake/CLI/Main.lean
View file

@ -379,23 +379,23 @@ protected def help : CliM PUnit := do
end lake
def lakeCli : (cmd : String) → CliM PUnit
| "new" => lake.new
| "init" => lake.init
| "build" => lake.build
| "update" => lake.update
| "resolve-deps" => lake.resolveDeps
| "upload" => lake.upload
| "print-paths" => lake.printPaths
| "clean" => lake.clean
| "script" => lake.script
| "scripts" => lake.script.list
| "run" => lake.script.run
| "serve" => lake.serve
| "env" => lake.env
| "exe" => lake.exe
| "self-check" => lake.selfCheck
| "help" => lake.help
| cmd => throw <| CliError.unknownCommand cmd
| "new" => lake.new
| "init" => lake.init
| "build" => lake.build
| "update" | "upgrade" => lake.update
| "resolve-deps" => lake.resolveDeps
| "upload" => lake.upload
| "print-paths" => lake.printPaths
| "clean" => lake.clean
| "script" => lake.script
| "scripts" => lake.script.list
| "run" => lake.script.run
| "serve" => lake.serve
| "env" => lake.env
| "exe" | "exec" => lake.exe
| "self-check" => lake.selfCheck
| "help" => lake.help
| cmd => throw <| CliError.unknownCommand cmd
def lake : CliM PUnit := do
match (← getArgs) with