From 3b28d24319a431ea4fd16aefc3371b4936b09cc2 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 3 Oct 2021 12:40:58 -0400 Subject: [PATCH] refactor: make package `name` a `Name` --- Lake/BuildPackage.lean | 4 ++-- Lake/Init.lean | 22 +++++++++++----------- Lake/Package.lean | 38 +++++++++++++++++++++++++------------- Lake/Resolve.lean | 7 ++++--- README.md | 6 +++--- examples/init/clean.sh | 4 ++-- examples/init/test.sh | 16 ++++++++-------- 7 files changed, 55 insertions(+), 42 deletions(-) diff --git a/Lake/BuildPackage.lean b/Lake/BuildPackage.lean index e3e95a14ac..fe30fa7d3b 100644 --- a/Lake/BuildPackage.lean +++ b/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 diff --git a/Lake/Init.lean b/Lake/Init.lean index ad790ccdd7..a8fa95cd30 100644 --- a/Lake/Init.lean +++ b/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 diff --git a/Lake/Package.lean b/Lake/Package.lean index 486f886ed5..2d74b5b48f 100644 --- a/Lake/Package.lean +++ b/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. -/ diff --git a/Lake/Resolve.lean b/Lake/Resolve.lean index 81ea082270..abe53cfe7d 100644 --- a/Lake/Resolve.lean +++ b/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})" diff --git a/README.md b/README.md index 54cf68abfa..90427e66d0 100644 --- a/README.md +++ b/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 [-- ]`. * `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). diff --git a/examples/init/clean.sh b/examples/init/clean.sh index b800fa44e5..b096e8abc2 100755 --- a/examples/init/clean.sh +++ b/examples/init/clean.sh @@ -1,2 +1,2 @@ -rm -rf helloNew -rm -rf helloInit +rm -rf hello-world +rm -rf hello_world diff --git a/examples/init/test.sh b/examples/init/test.sh index 2e59ec56a0..51f1c782b9 100755 --- a/examples/init/test.sh +++ b/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