diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean index 0a17c98ab691..5f2e36e371bc 100644 --- a/src/lake/Lake/Config/LeanLibConfig.lean +++ b/src/lake/Lake/Config/LeanLibConfig.lean @@ -27,13 +27,11 @@ structure LeanLibConfig extends LeanConfig where /-- The root module(s) of the library. - Submodules of these roots (e.g., `Lib.Foo` of `Lib`) are considered - part of the package. - - Defaults to a single root of the library's upper camel case name. + part of the library. + Defaults to a single root of the target's name. -/ - roots : Array Name := #[toUpperCamelCase name] + roots : Array Name := #[name] /-- An `Array` of module `Glob`s to build for the library. @@ -48,9 +46,9 @@ structure LeanLibConfig extends LeanConfig where /-- 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. + Defaults to the name of the target. -/ - libName := toUpperCamelCase name |>.toString (escape := false) + libName := name.toString (escape := false) /-- An `Array` of target names to build before the library's modules. -/ extraDepTargets : Array Name := #[] diff --git a/src/lake/README.md b/src/lake/README.md index 04ec9d9814f3..9cabf5a4b2b3 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -200,9 +200,9 @@ lean_lib «target-name» where **Configuration Options** * `srcDir`: The subdirectory of the package's source directory containing the library's source files. Defaults to the package's `srcDir`. (This will be passed to `lean` as the `-R` option.) -* `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. +* `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 target's name. * `globs`: An `Array` of module `Glob`(s) to build for the library. The term `glob` comes from [file globs](https://en.wikipedia.org/wiki/Glob_(programming)) (e.g., `foo/*`) on Unix. A submodule glob builds every Lean source file within the module's directory (i.e., ``Glob.submodules `Foo`` is essentially equivalent to a theoretical `import Foo.*`). Local imports of glob'ed files (i.e., fellow modules of the workspace) are also recursively built. Defaults to a `Glob.one` of each of the library's `roots`. -* `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. +* `libName`: The `String` name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the name of the target. * `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). diff --git a/src/lake/examples/precompile/foo/lakefile.lean b/src/lake/examples/precompile/foo/lakefile.lean index 66d352977562..a7642b102b0e 100644 --- a/src/lake/examples/precompile/foo/lakefile.lean +++ b/src/lake/examples/precompile/foo/lakefile.lean @@ -6,4 +6,4 @@ package foo { } @[default_target] -lean_lib foo +lean_lib Foo diff --git a/src/lake/examples/targets/lakefile.lean b/src/lake/examples/targets/lakefile.lean index 20336f9d51b9..54ce413e6a23 100644 --- a/src/lake/examples/targets/lakefile.lean +++ b/src/lake/examples/targets/lakefile.lean @@ -6,17 +6,14 @@ package targets { } @[default_target] -lean_lib foo { +lean_lib Foo where defaultFacets := #[LeanLib.staticFacet] -} -lean_lib bar { +lean_lib Bar where defaultFacets := #[LeanLib.sharedFacet] -} -lean_lib baz { +lean_lib Baz where extraDepTargets := #[`caw] -} lean_exe a lean_exe b diff --git a/src/lake/examples/targets/test.sh b/src/lake/examples/targets/test.sh index ed74289c28dd..a05c2dcbef33 100755 --- a/src/lake/examples/targets/test.sh +++ b/src/lake/examples/targets/test.sh @@ -17,17 +17,17 @@ fi ./clean.sh # Test error on nonexistent facet -! $LAKE build targets:noexistent +$LAKE build targets:noexistent && false || true # Test custom targets and package, library, and module facets -$LAKE build bark | grep -m1 Bark! -$LAKE build targets/bark_bark | grep -m1 Bark! -$LAKE build targets:print_name | grep -m1 targets -$LAKE build Foo.Bar:print_src | grep -m1 Bar.lean -$LAKE build foo:print_name | grep -m1 foo +$LAKE build bark | grep Bark! +$LAKE build targets/bark_bark | grep Bark! +$LAKE build targets:print_name | grep targets +$LAKE build Foo.Bar:print_src | grep Bar.lean +$LAKE build Foo:print_name | grep Foo # Test the module `deps` facet -$LAKE build Foo:deps +$LAKE build +Foo:deps test -f ./.lake/build/lib/Foo/Bar.olean test ! -f ./.lake/build/lib/Foo.olean @@ -38,7 +38,7 @@ test -f ./.lake/build/lib/Foo/Baz.olean # Test `.c.o` specifier test ! -f ./.lake/build/ir/Bar.c.o -$LAKE build Bar:o +$LAKE build +Bar:c.o test -f ./.lake/build/ir/Bar.c.o # Test default targets @@ -50,26 +50,26 @@ $LAKE build targets/ ./.lake/build/bin/c test -f ./.lake/build/lib/Foo.olean test -f ./.lake/build/lib/${LIB_PREFIX}Foo.a -cat ./.lake/build/meow.txt | grep -m1 Meow! +cat ./.lake/build/meow.txt | grep Meow! # Test shared lib facets test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT test ! -f ./.lake/build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT -$LAKE build foo:shared bar +$LAKE build Foo:shared Bar test -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT test -f ./.lake/build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT # Test dynlib facet test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo-1.$SHARED_LIB_EXT -$LAKE build Foo:dynlib +$LAKE build +Foo:dynlib test -f ./.lake/build/lib/${LIB_PREFIX}Foo-1.$SHARED_LIB_EXT # Test library `extraDepTargets` test ! -f ./.lake/build/caw.txt test ! -f ./.lake/build/lib/Baz.olean -$LAKE build baz +$LAKE build Baz test -f ./.lake/build/lib/Baz.olean -cat ./.lake/build/caw.txt | grep -m1 Caw! +cat ./.lake/build/caw.txt | grep Caw! # Test executable build $LAKE build a b @@ -77,4 +77,4 @@ $LAKE build a b ./.lake/build/bin/b # Test repeat build works -$LAKE build bark | grep -m1 Bark! +$LAKE build bark | grep Bark!