refactor: lake: use plain lib name for root and native name

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 := #[]

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).

src/lake/examples/precompile/foo/lakefile.lean

@@ -6,4 +6,4 @@ package foo {
 }
 
 @[default_target]
-lean_lib foo
+lean_lib Foo

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

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,31 +50,31 @@ $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
 ./.lake/build/bin/a
 ./.lake/build/bin/b
 
 # Test repeat build works
-$LAKE build bark | grep -m1 Bark!
+$LAKE build bark | grep Bark!