refactor: lake server -> lake serve

This commit is contained in:
tydeu 2021-11-25 05:29:47 -05:00
parent 63bd325b3b
commit 2092850b02
2 changed files with 5 additions and 5 deletions

View file

@ -62,11 +62,11 @@ errors and prints the list of available scripts.
You can pass -h/--help after the script name to print its docstring."
def helpServer :=
def helpServe :=
"Start the Lean language server
USAGE:
lake server [-- <args>...]
lake serve [-- <args>...]
Run the language server of the Lean installation (i.e., via `lean --server`)
with the package configuration's `moreServerArgs` field and `args`.
@ -131,7 +131,7 @@ def helpCmd : (cmd : String) → String
| "new" => helpNew
| "init" => helpInit
| "run" => helpRun
| "server" => helpServer
| "serve" => helpServe
| "configure" => helpConfigure
| "build" => helpBuild
| "clean" => helpClean

View file

@ -232,7 +232,7 @@ def printPaths (imports : List String := []) : CliM PUnit := do
else
exit noConfigFileCode
def server (leanInstall : LeanInstall) (pkg : Package) (args : List String) : CliM PUnit := do
def serve (leanInstall : LeanInstall) (pkg : Package) (args : List String) : CliM PUnit := do
let child ← IO.Process.spawn {
cmd := leanInstall.lean.toString,
args := #["--server"] ++ pkg.moreServerArgs ++ args
@ -246,7 +246,7 @@ def command : (cmd : String) → CliM PUnit
| "new" => do noArgsRem <| new (← takeArg)
| "init" => do noArgsRem <| init (← takeArg)
| "run" => do noArgsRem <| script (← loadPkg []) (← takeArg) (← getSubArgs)
| "server" => do noArgsRem <| server (← getLeanInstall) (← loadPkg []) (← getSubArgs)
| "serve" => do noArgsRem <| serve (← getLeanInstall) (← loadPkg []) (← getSubArgs)
| "configure" => do noArgsRem <| configure (← loadPkg (← getSubArgs))
| "print-paths" => do printPaths (← takeArgs)
| "build" => do runBuildM (← loadPkg (← getSubArgs)) <| build (← takeArgs)