diff --git a/README.md b/README.md index 1d9eb93ba1..ec662b1e99 100644 --- a/README.md +++ b/README.md @@ -170,9 +170,9 @@ lean_lib «target-name» { **Configuration Options** * `srcDir`: The subdirectory of the package' source directory containing the library's source files. Defaults simply to said `srcDir`. (This will be passed to `lean` as the `-R` option.) -* `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. +* `roots`: An `Array` of root module `Name`(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. +* `libName`: The `String` 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. * `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) @@ -191,8 +191,8 @@ lean_exe «target-name» { **Configuration Options** -* `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 `-`. +* `root`: The root module `Name` 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 `String` 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`. * `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).