From a4622f61caee7cdd81d9ca1b06bad2ac503b7409 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 8 Jul 2021 20:58:25 -0400
Subject: [PATCH] doc: update help command text

---
 Lake/Cli.lean | 70 +++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 51 insertions(+), 19 deletions(-)

diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 3daddd06db..799f0680e3 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -9,18 +9,27 @@ import Lake.LeanConfig
 
 namespace Lake
 
+def version.major := 2
+def version.minor := 0
+def version.isPre := true
+def versionString := s!"{version.major}.{version.minor}-pre"
+
 def usage :=
-"Lake, version " ++ uiLeanVersionString ++ "
-Usage: lake <command>
+"Lake, version " ++ versionString ++ "
+
+Usage: 
+  lake <command>
 
 init <name>      create a Lean package in the current directory
 configure        download and build dependencies
-build [<args>]   configure and build *.olean files
+build            configure and build *.olean files
+build-lib        configure and build a static library
+build-bin        configure and build a native binary executable
 
 See `lake help <command>` for more information on a specific command."
 
 def helpConfigure :=
-"Download dependencies
+"Download and build dependencies
 
 Usage:
   lake configure
@@ -33,24 +42,45 @@ versions of the same package, the version materialized is undefined. No copy
 is made of local dependencies."
 
 def helpBuild :=
-"Download dependencies and build *.olean files
+"Configure this package and build *.olean files
 
 Usage:
-  lake build [<leanmake-args>] [-- <lean-args>]
+  lake build
 
-This command invokes `lake configure` followed by `leanmake <leanmake-args> LEAN_OPTS=<lean-args>`.
-If defined, the `package.timeout` configuration value is passed to Lean via its `-T` parameter.
-If no <lean-args> are given, only .olean files will be produced in `build/`. If `lib` or `bin`
-is passed instead, the extracted C code is compiled with `c++` and a static library in `build/lib`
-or an executable in `build/bin`, respectively, is created. `lake build bin` requires a declaration
-of name `main` in the root namespace, which must return `IO Unit` or `IO UInt32` (the exit code) and
-may accept the program's command line arguments as a `List String` parameter.
+This command configures the package's dependencies and then builds the package 
+with `lean`. Additional arguments can be passed to `lean` by setting the 
+`leanArgs` field in the package's configuration."
 
-NOTE: building and linking dependent libraries currently has to be done manually, e.g.
-```
-$ (cd a; lake build lib)
-$ (cd b; lake build bin LINK_OPTS=../a/build/lib/libA.a)
-```"
+def helpBuildLib :=
+"Configure this package and build a static library
+
+Usage:
+  lake build-lib
+
+This command configures this package's dependencies, builds the package itself,
+compiles the extracted C code with `leanc`, and uses `ar` to produce a static 
+library in  `build/lib`. 
+
+Additional arguments can be passed to `lean` or `leanc` by setting the 
+`leanArgs` or `leancArgs` fields in the package's configuration."
+
+def helpBuildBin :=
+"Configure the package and build a native binary executable
+
+Usage:
+  lake build-bin
+
+This command configures this package's dependencies, builds the package itself,
+compiles the extracted C code `leannc`, and then links the object files with 
+`leanc` to produce a native binary executable in `build/bin`. 
+
+This requires a declaration of name `main` in the root namespace, which must 
+return `IO Unit` or `IO UInt32` (the exit code) and may accept the program's 
+command line arguments as a `List String` parameter.
+
+Additional  arguments can be passed to `lean`, the  `leanc` compiler, or the 
+`leanc` linker by setting the `leanArgs`, `leancArgs`, or `linkArgs` fields in 
+the package's configuration."
 
 def helpInit :=
 "Create a new Lean package in the current directory
@@ -73,11 +103,13 @@ def cli : (cmd : String) → (lakeArgs pkgArgs : List String) → IO Unit
 | "configure",    [],             []  => do configure (← getRootPkg)
 | "print-paths",  imports,        []  => do printPaths (← getRootPkg) imports
 | "build",        [],             []  => do build (← getRootPkg)
-| "build-bin",    [],             []  => do discard <| buildBin (← getRootPkg) 
 | "build-lib",    [],             []  => do discard <| buildStaticLib (← getRootPkg)
+| "build-bin",    [],             []  => do discard <| buildBin (← getRootPkg) 
 | "help",         ["init"],       []  => IO.println helpInit
 | "help",         ["configure"],  []  => IO.println helpConfigure
 | "help",         ["build"],      []  => IO.println helpBuild
+| "help",         ["build-lib"],  []  => IO.println helpBuildLib
+| "help",         ["build-bin"],  []  => IO.println helpBuildBin
 | "help",         _,              []  => IO.println usage
 | _,              _,              _   => throw <| IO.userError usage