refactor: make package name a Name

Lake/BuildPackage.lean

@@ -120,7 +120,7 @@ def recBuildPackageWithDeps
 : RecBuild Package (Array ActivePackageTarget) m := fun pkg buildPkg => do
   let mut depTargets := #[]
   for dep in pkg.dependencies do
-    let targets? ← fetch? dep.name.toName
+    let targets? ← fetch? dep.name
     let targets ← do
       if let some targets := targets? then
         pure targets
@@ -133,7 +133,7 @@ def recBuildPackageWithDeps
 
 def buildPackageTargetsWithDeps (pkgs : Array Package) : BuildM (Array ActivePackageTarget) := do
   failOnBuildCycle <| ← RBTopT.run' <| pkgs.concatMapM fun pkg =>
-    buildRBTop (cmp := Name.quickCmp) recBuildPackageWithDeps (·.name.toName) pkg
+    buildRBTop (cmp := Name.quickCmp) recBuildPackageWithDeps Package.name pkg
 
 def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
   (← buildPackageTargetsWithDeps #[self]).back

Lake/Init.lean

@@ -9,6 +9,7 @@ import Lake.LeanConfig
 
 namespace Lake
 open Git System
+open Lean (Name)
 
 /-- `elan` toolchain file name -/
 def toolchainFileName : FilePath :=
@@ -17,17 +18,14 @@ def toolchainFileName : FilePath :=
 def gitignoreContents :=
 s!"/{defaultBuildDir}\n/{defaultDepsDir}\n"
 
-def libFileName (libName : String) : FilePath :=
-  s!"{libName}.lean"
-
 def libFileContents :=
   s!"def hello := \"world\""
 
 def mainFileName : FilePath :=
   s!"{defaultBinRoot}.lean"
 
-def mainFileContents (libName : String) :=
-s!"import {libName.toName.toString}
+def mainFileContents (libRoot : Name) :=
+s!"import {libRoot}
 
 def main : IO Unit :=
   IO.println s!\"Hello, \{hello}!\"
@@ -38,7 +36,7 @@ s!"import Lake
 open Lake DSL
 
 package \{
-  name := \"{pkgName}\"
+  name := `{pkgName.toName}
 }
 "
 
@@ -53,13 +51,14 @@ def initPkg (dir : FilePath) (name : String) : IO PUnit := do
   IO.FS.writeFile configFile (pkgConfigFileContents name)
 
   -- write example code if the files do not already exist
-  let libName := name.capitalize
-  let libFile := dir / libFileName libName
+  let libRoot := toUpperCamelCase name.toName
+  let libFile := Lean.modToFilePath dir libRoot "lean"
   unless (← libFile.pathExists) do
+    IO.FS.createDirAll libFile.parent.get!
     IO.FS.writeFile libFile libFileContents
   let mainFile := dir / mainFileName
   unless (← mainFile.pathExists) do
-    IO.FS.writeFile mainFile <| mainFileContents libName
+    IO.FS.writeFile mainFile <| mainFileContents libRoot
 
   -- write current toolchain to file for `elan`
   IO.FS.writeFile (dir / toolchainFileName) <| leanVersionString ++ "\n"
@@ -81,5 +80,6 @@ def init (pkgName : String) : IO PUnit :=
   initPkg "." pkgName
 
 def new (pkgName : String) : IO PUnit := do
-  IO.FS.createDir pkgName
-  initPkg pkgName pkgName
+  let dirName := pkgName.map fun chr => if chr == '.' then '-' else chr
+  IO.FS.createDir dirName
+  initPkg dirName pkgName

Lake/Package.lean

@@ -60,10 +60,10 @@ deriving Inhabited, Repr
 /-- A `Dependency` of a package. -/
 structure Dependency where
   /--
-    A name for the dependency.
+    A `Name` for the dependency.
     The names of a package's dependencies cannot clash.
   -/
-  name : String
+  name : Name
   /--
     The source of a dependency.
     See the documentation of `Source` for more information.
@@ -87,6 +87,18 @@ deriving Inhabited, Repr
 -/
 abbrev Script := (args : List String) → IO UInt32
 
+/-- Converts a snake case, kebab case, or lower camel case `String` to upper camel case. -/
+def toUpperCamelCaseString (str : String) : String :=
+  let parts := str.split fun chr => chr == '_' || chr == '-'
+  String.join <| parts.map (·.capitalize)
+
+/-- Converts a snake case, kebab case, or lower camel case `Name` to upper camel case. -/
+def toUpperCamelCase (name : Name) : Name :=
+  if let Name.str p s _ := name then
+    Name.mkStr (toUpperCamelCase p) <| toUpperCamelCaseString s
+  else
+    name
+
 --------------------------------------------------------------------------------
 -- # PackageConfig
 --------------------------------------------------------------------------------
@@ -95,9 +107,9 @@ abbrev Script := (args : List String) → IO UInt32
 structure PackageConfig where
 
   /--
-    The name of the package.
+    The `Name` of the package.
   -/
-  name : String
+  name : Name
 
   /--
     A `HashMap` of scripts for the package.
@@ -153,9 +165,9 @@ structure PackageConfig where
     Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered
     part of the package.
 
-    Defaults to a single root of the package's uppercase `name`.
+    Defaults to a single root of the package's upper camel case `name`.
   -/
-  libRoots : Array Name := #[name.capitalize]
+  libRoots : Array Name := #[toUpperCamelCase name]
 
   /--
     An `Array` of module `Glob`s to build for the package's library.
@@ -188,9 +200,9 @@ structure PackageConfig where
 
   /--
     The name of the package's static library.
-    Defaults to the package's uppercase `name`.
+    Defaults to the package's upper camel case `name`.
   -/
-  libName : String := name.capitalize
+  libName : String := toUpperCamelCase name |>.toString (escape := false)
 
   /--
     The build subdirectory to which Lake should output the package's static library.
@@ -200,13 +212,13 @@ structure PackageConfig where
 
   /--
     The name of the package's binary executable.
-    Defaults to the package's `name`.
+    Defaults to the package's `name` with any `.` replaced with a `-`.
   -/
-  binName : String := name
+  binName : String := name.toStringWithSep "-" (escape := false)
 
   /--
-    The name of the package's binary executable.
-    Defaults to the package's `name`.
+    The build subdirectory to which Lake should output the package's binary executable.
+    Defaults to `defaultBinDir` (i.e., `bin`).
   -/
   binDir : FilePath := defaultBinDir
 
@@ -268,7 +280,7 @@ def IOPackager := (pkgDir : FilePath) → (args : List String) → IO PackageCon
 namespace Package
 
 /-- The package's `name` configuration. -/
-def name (self : Package) : String :=
+def name (self : Package) : Name :=
   self.config.name
 
 /-- The package's `scripts` configuration. -/

Lake/Resolve.lean

@@ -40,8 +40,9 @@ def materializeDep (pkg : Package) (dep : Dependency) : IO FilePath :=
     let depDir := pkg.dir / dir
     depDir
   | Source.git url rev branch => do
-    let depDir := pkg.depsDir / dep.name
-    materializeGitDep dep.name depDir url rev branch
+    let name := dep.name.toString (escape := false)
+    let depDir := pkg.depsDir / name
+    materializeGitDep name depDir url rev branch
     depDir
 
 /--
@@ -51,7 +52,7 @@ def materializeDep (pkg : Package) (dep : Dependency) : IO FilePath :=
 def resolveDep (pkg : Package) (dep : Dependency) : IO Package := do
   let dir ← materializeDep pkg dep
   let depPkg ← Package.fromDir (dir / dep.dir) dep.args
-  unless depPkg.name = dep.name do
+  unless depPkg.name == dep.name do
     throw <| IO.userError <|
       s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
       s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})"

README.md

@@ -65,7 +65,7 @@ import Lake
 open Lake DSL
 
 package {
-  name := "hello"
+  name := `hello
 }
 ```
 
@@ -86,7 +86,7 @@ Lake provides a large assortment of configuration options for packages.
 
 ### General
 
-* `name` **(Required)**: The name of the package.
+* `name` **(Required)**: The `Name` of the package.
 * `scripts`: A `HashMap` of scripts for the package. A `Script` is an arbitrary `(args : List String) → IO UInt32` function that is indexed by a `String` key and can be be run by `lake run <key> [-- <args>]`.
 * `dependencies`: An `Array` of the package's dependencies.
 * `depsDir`: The directory to which Lake should download dependencies. Defaults to `lean_packages`.
@@ -104,7 +104,7 @@ Lake provides a large assortment of configuration options for packages.
 * `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`.
 * `libName`: The name of the package's static library. Defaults to the string representation of the package's `moduleRoot`.
 * `libDir`: The build subdirectory to which Lake should output the package's static library. Defaults to `lib`.
-* `binName`: The name of the package's binary executable. Defaults to the package's `name`.
+* `binName`: The name of the package's binary executable. Defaults to the package's `name` with any `.` replaced with a `-`.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executable. Defaults to `bin`.
 * `binRoot`: The root module of the package's binary executable. Defaults to `Main`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper.
 * `moreLibTargets`: Additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables).

examples/init/clean.sh

@@ -1,2 +1,2 @@
-rm -rf helloNew
-rm -rf helloInit
+rm -rf hello-world
+rm -rf hello_world

examples/init/test.sh

@@ -4,23 +4,23 @@ set -ex
 
 # Test `new`
 
-${LAKE:-../../build/bin/lake} new helloNew
+${LAKE:-../../build/bin/lake} new hello.world
 
-cd helloNew
+cd hello-world
 test -f lean-toolchain
 ${LAKE:-../../../build/bin/lake} build-bin
-./build/bin/helloNew
+./build/bin/hello-world
 cd ..
 
 # Test `init`
 
-mkdir helloInit
+mkdir hello_world
 
-cd helloInit
-${LAKE:-../../../build/bin/lake} init helloInit
+cd hello_world
+${LAKE:-../../../build/bin/lake} init hello_world
 ${LAKE:-../../../build/bin/lake} build-bin
-./build/bin/helloInit
+./build/bin/hello_world
 
 # Test `init` on existing package (should error)
 
-${LAKE:-../../../build/bin/lake} init helloInit && exit 1 || true
+${LAKE:-../../../build/bin/lake} init hello_world && exit 1 || true