feat: add shorthands for lake script run/list

closes #88
leanprover · Jul 9, 2022 · 080cda1 · 080cda1
1 parent 505104c
commit 080cda1
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 6 deletions.
diff --git a/Lake/CLI/Help.lean b/Lake/CLI/Help.lean
@@ -28,6 +28,8 @@ COMMANDS:
   update                update dependencies
   clean                 remove build outputs
   script                manage and run workspace scripts
+  scripts               shorthand for `lake script list`
+  run <script>          shorthand for `lake script run`
   serve                 start the Lean language server
   env <cmd> [<args>...] execute a command in the workspace's environment
 
@@ -196,6 +198,8 @@ def help : (cmd : String) → String
 | "update"    => helpUpdate
 | "clean"     => helpClean
 | "script"    => helpScriptCli
+| "scripts"   => helpScriptList
+| "run"       => helpScriptRun
 | "serve"     => helpServe
 | "env"       => helpEnv
 | _           => usage
diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
@@ -400,6 +400,8 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "print-paths" => lake.printPaths
 | "clean"       => lake.clean
 | "script"      => lake.script
+| "scripts"     => lake.script.list
+| "run"         => lake.script.run
 | "serve"       => lake.serve
 | "env"         => lake.env
 | "self-check"  => lake.selfCheck

diff --git a/examples/scripts/test.sh b/examples/scripts/test.sh
@@ -1,7 +1,9 @@
 set -ex
-${LAKE:-../../build/bin/lake} script list
-${LAKE:-../../build/bin/lake} script run scripts/greet
-${LAKE:-../../build/bin/lake} script run greet me
-${LAKE:-../../build/bin/lake} script doc greet
-${LAKE:-../../build/bin/lake} script run nonexistant && false || true
-${LAKE:-../../build/bin/lake} script doc nonexistant && false || true
+LAKE=${LAKE:-../../build/bin/lake}
+$LAKE script list
+$LAKE run scripts/greet
+$LAKE script run greet me
+$LAKE script doc greet
+$LAKE script run nonexistant && false || true
+$LAKE script doc nonexistant && false || true
+$LAKE scripts