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

doc: update help command text

Browse source
This commit is contained in:
tydeu 2021-07-08 20:58:25 -04:00
parent 981db940e8
commit a4622f61ca
1 changed files with 51 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
Lake/Cli.lean
View file

@ -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