From 0bb6bcf24cfafaad564a3dbacd1a5f9fc19cbb4b Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 11 Sep 2023 19:25:23 -0400
Subject: [PATCH] feat: lake: add `upgrade` and `exec` CLI aliases

---
 src/lake/Lake/CLI/Help.lean | 42 ++++++++++++++++++++++---------------
 src/lake/Lake/CLI/Main.lean | 34 +++++++++++++++---------------
 2 files changed, 42 insertions(+), 34 deletions(-)

diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index 023295b0db..0d9b9e5a97 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -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
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index a1f8f63239..50b1427dd3 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -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