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

doc: update defaultFacet description

Browse source
This commit is contained in:
tydeu 2022-06-10 16:13:55 -04:00
parent 05b4a8fc76
commit 7ea84c5961
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Config/Package.lean
View file

@ -86,7 +86,7 @@ structure PackageConfig extends WorkspaceConfig where
/--
The optional `PackageFacet` to build on a bare `lake build` of the package.
Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`.
Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`, or `none`.
Defaults to `exe`. See `lake help build` for more info on build facets.
**DEPRECATED:**

2
README.md
View file

@ -117,7 +117,7 @@ Workspace options are shared across a package and its dependencies.
* `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 `bin`, `staticLib`, `sharedLib`, or `oleans`. 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.
* `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.
## Defining Build Targets