doc: update README

Lake/Config/LeanLibConfig.lean

@@ -62,7 +62,7 @@ structure LeanLibConfig extends LeanConfig where
   precompileModules : Bool := false
 
   /--
-  The set of module facets to build and combine into the library's static
+  An `Array` of module facets to build and combine into the library's static
   and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file
   compiled from the Lean source).
   -/

README.md

@@ -16,6 +16,7 @@ Each `lakefile.lean` includes a `package` declaration (akin to `main`) which def
   + [Lean Libraries](#lean-libraries)
   + [Binary Executables](#binary-executables)
   + [External Libraries](#external-libraries)
+  + [Custom Targets](#custom-targets)
 * [Adding Dependencies](#adding-dependencies)
   + [Syntax of `require`](#syntax-of-require)
 * [Writing and Running Scripts](#writing-and-running-scripts)
@@ -31,7 +32,7 @@ Note that the Lake included with Lean is not updated as frequently as this repos
 
 ## Creating and Building a Package
 
-To create a new package, either run `lake init <package-name>` to setup the package in the current directory or `lake new <package-name>` to create it in a new directory. For example, we could create the package `hello` like so:
+To create a new package, either run `lake init <package-name> [<template>]` to setup the package in the current directory or `lake new <package-name> [<template>]` to create it in a new directory. For example, we could create the package `hello` like so:
 
 ```
 $ mkdir hello
@@ -94,7 +95,7 @@ $ ./build/bin/hello
 Hello, world!
 ```
 
-Examples of different package configurations can be found in the [`examples`](examples) folder of this repository.
+Examples of different package configurations can be found in the [`examples`](examples) folder of this repository. You can also specified a particular configuration file template when using `lake init` or `lake new` to control what files Lake creates. See `lake help init` or `lake help new` for details.
 
 ## Package Configuration Options
 
@@ -114,14 +115,14 @@ Workspace options are shared across a package and its dependencies.
 * `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`.
 * `libDir`: The build subdirectory to which Lake should output the package's libraries. Defaults to `lib`.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executables. Defaults to `bin`.
-* `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. `Target.collectOpaqueList/collectOpaqueArray` can be used combine multiple extra targets into a single `extraDepTarget`.
 * `precompileModules`:  Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`.
 * `isLeanOnly`: Whether the package is "Lean-only". A Lean-only package does not produce native files for modules (e.g. `.c`, `.o`). Defaults to `false`. Setting `precompileModules` to `true` will override this setting and produce native files anyway (as they are needed to build module dynlibs).
 * `moreServerArgs`:  Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`.
+* `buildType`: The `BuildType` of targets in the package (see [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670)). One of `debug`, `relWithDebInfo`, `minSizeRel`, or `release`. Defaults to `release`.
 * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files.
-* `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes `-O3` and `-DNDEBUG` automatically, but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
-* `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' Lean libraries) to build and link to the package's binaries (and to dependent packages' binaries). **DEPRECATED:** Use separate [`extern_lib`](#external-libraries) targets instead.
-* `defaultFacet`: The `PackageFacet` to build on a bare `lake build` of the package. Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`, or `none`. Defaults to `exe`. See `lake help build` for more info on build facets. **DEPRECATED:** Package facets will be removed in a future version of Lake. Use a separate [`lean_lib`](#lean-libraries) or [`lean_exe`](#binary-executables) default target instead.
+* `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes some flags based on the `buildType`, but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
+* `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` when linking (e.g., binary executables or shared libraries). These will come *after* the paths of `extern_lib` targets.
+* `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. `Target.collectOpaqueList/collectOpaqueArray` can be used combine multiple extra targets into a single `extraDepTarget`. **DEPRECATED:** Try to use separate [custom target declarations](#custom-targets) instead. Otherwise, raise an issue here about your use case.
 
 ## Defining Build Targets
 
@@ -144,8 +145,9 @@ lean_lib «target-name» {
 * `roots`: The root module(s) of the library. Submodules of these roots (e.g., `Lib.Foo` of `Lib`) are considered part of the library. Defaults to a single root of the library's upper camel case name.
 * `globs`: An `Array` of module `Glob`s to build for the library. Defaults to a `Glob.one` of each of the library's  `roots`. Submodule globs build every source file within their directory. Local imports of glob'ed files (i.e., fellow modules of the workspace) are also recursively built.
 * `libName`: The name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the upper camel case name of the target.
-* `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` while linking the shared library. These will come *after* the paths of libraries built with the package's
-`moreLibTargets`.
+* `nativeFacets`: An `Array` of module facets to build and combine into the library's static
+and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source). **PREVIEW:** Module facets are in beta, unstable, and not yet documented. Use with care.
+* `precompileModules`, `buildType`, `moreLeanArgs`, `moreLinkArgs`, `moreLinkArgs`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest)
 
 ### Binary Executables
 
@@ -164,7 +166,7 @@ lean_exe «target-name» {
 * `root`: The root module of the binary executable. Should include a `main` definition that will serve as the entry point of the program. The root is built by recursively building its local imports (i.e., fellow modules of the workspace). Defaults to the name of the target.
 * `exeName`: The name of the binary executable. Defaults to the target name with any `.` replaced with a `-`.
 * `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`.
-* `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` when linking the binary executable. These will come *after* the paths of libraries built with the package's `moreLibTargets`.
+* `buildType`, `moreLeanArgs`, `moreLinkArgs`, `moreLinkArgs`: Augments the package's corresponding configuration option. The executable's arguments come after and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest).
 
 ### External Libraries
 
@@ -177,6 +179,17 @@ extern_lib «target-name» :=
   -- term of type `FileTarget` that builds the external library
 ```
 
+### Custom Targets
+
+A arbitrary target that can be built via `lake build <target-name>`.
+
+**Syntax**
+
+```lean
+target «target-name» : α :=
+  -- term of type `BuildTarget α` that builds the target
+```
+
 ## Adding Dependencies
 
 Lake packages can have dependencies. Dependencies are other Lake packages the current package needs in order to function. They can be sourced directly from a local folder (e.g., a subdirectory of the package) or come from remote Git repositories. For example, one can depend on the Lean 4 port of [mathlib](https://github.com/leanprover-community/mathlib4) like so:
@@ -185,11 +198,13 @@ Lake packages can have dependencies. Dependencies are other Lake packages the cu
 package hello
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"master"
+  "https://github.com/leanprover-community/mathlib4.git"
 ```
 
 The next run of `lake build` (or refreshing dependencies in an editor like VSCode) will clone the mathlib repository and build it. Information on the specific revision cloned will then be saved to `manifest.json` in the workspace's `packageDir` (by default, `lean_packages`) to enable reproducibility. To update `mathlib` after this, you will need to run `lake update` -- other commands do not update resolved dependencies.
 
+For a theorem proving packages which depend on `mathlib`, you can also run `lake new <package-name> math` to generate a package configuration file that already has the `mathlib` dependency (and no binary executable target).
+
 ### Syntax of `require`
 
 The `require` command has two forms: