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

fix: lake: lock test timeout + README typos

Browse source
This commit is contained in:
tydeu 2023-08-10 11:02:22 -04:00 • committed by Mac Malone
parent 75a9284320
commit 06853e5c3b
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/lake/README.md
View file

@ -185,7 +185,7 @@ lean_lib «target-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 `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.
* `extraDepTargets`: An `Array` of [target](#custom-targets) names that to build before the library's modules.
* `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the library's modules.
* `defaultFacets`: An `Array` of library facets to build on a bare `lake build` of the library. For example, setting this to `#[LeanLib.sharedLib]` will build the shared library facet.
* `nativeFacets`: An `Array` of [module facets](#defining-new-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).
* `precompileModules`, `buildType`, `moreLeanArgs`, `weakLeanArgs`, `moreLeancArgs`, `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)
@ -207,7 +207,7 @@ lean_exe «target-name» {
* `srcDir`: The subdirectory of the package's source directory containing the executable's source file. Defaults to the package's `srcDir`. (This will be passed to `lean` as the `-R` option.)
* `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 `-`.
* `extraDepTargets`: An `Array` of [target](#custom-targets) names that to build before the executable's modules.
* `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the executable's modules.
* `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the executable. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source).
* `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`, `weakLeanArgs`, `moreLeancArgs`, `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).

1
src/lake/test/lock/test.sh
View file

@ -12,6 +12,7 @@ fi
./clean.sh
# Test lock file creation on build
touch test.log
$LAKE build Loop 2>&1 > test.log &
grep -q "Building" < <($TAIL --pid=$$ -f test.log)
kill %%