From a093a38459ca47ebe387f2bf78ae6f006fcd18ec Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 26 Sep 2021 18:45:31 -0400 Subject: [PATCH] refactor: rename `package.lean` to `lakefile.lean` --- Lake/Cli.lean | 2 +- Lake/Init.lean | 10 +++++----- Lake/LeanConfig.lean | 8 +++++--- Lake/Package.lean | 2 +- README.md | 4 ++-- examples/bootstrap/{package.lean => lakefile.lean} | 0 examples/deps/a/{package.lean => lakefile.lean} | 0 examples/deps/b/{package.lean => lakefile.lean} | 0 examples/deps/foo/{package.lean => lakefile.lean} | 0 examples/ffi-dep/{package.lean => lakefile.lean} | 0 examples/ffi/{package.lean => lakefile.lean} | 0 examples/git/{package.lean => lakefile.lean} | 4 +--- examples/hello/{package.lean => lakefile.lean} | 0 examples/io/{package.lean => lakefile.lean} | 0 examples/main/{package.lean => lakefile.lean} | 0 15 files changed, 15 insertions(+), 15 deletions(-) rename examples/bootstrap/{package.lean => lakefile.lean} (100%) rename examples/deps/a/{package.lean => lakefile.lean} (100%) rename examples/deps/b/{package.lean => lakefile.lean} (100%) rename examples/deps/foo/{package.lean => lakefile.lean} (100%) rename examples/ffi-dep/{package.lean => lakefile.lean} (100%) rename examples/ffi/{package.lean => lakefile.lean} (100%) rename examples/git/{package.lean => lakefile.lean} (61%) rename examples/hello/{package.lean => lakefile.lean} (100%) rename examples/io/{package.lean => lakefile.lean} (100%) rename examples/main/{package.lean => lakefile.lean} (100%) diff --git a/Lake/Cli.lean b/Lake/Cli.lean index 29707365f3..f2e752e54a 100644 --- a/Lake/Cli.lean +++ b/Lake/Cli.lean @@ -28,7 +28,7 @@ def Package.clean (self : Package) : IO PUnit := structure CliOptions where wantsHelp : Bool := false dir : FilePath := "." - file : FilePath := pkgFileName + file : FilePath := defaultConfigFile subArgs : List String := [] abbrev CliM := CliT (StateT CliOptions IO) diff --git a/Lake/Init.lean b/Lake/Init.lean index 7c29caa696..e0bf7842cc 100644 --- a/Lake/Init.lean +++ b/Lake/Init.lean @@ -25,7 +25,7 @@ def mainFileContents := IO.println \"Hello, world!\" " -def pkgFileContents (pkgName : String) := +def pkgConfigFileContents (pkgName : String) := s!"import Lake open Lake DSL @@ -38,11 +38,11 @@ package \{ def initPkg (dir : FilePath) (name : String) : IO PUnit := do -- write default configuration file - let pkgFile := dir / pkgFileName - if (← pkgFile.pathExists) then - -- error if package already has a `package.lean` + let configFile := dir / defaultConfigFile + if (← configFile.pathExists) then + -- error if package already has a `lakefile.lean` throw <| IO.userError "package already initialized" - IO.FS.writeFile pkgFile (pkgFileContents name) + IO.FS.writeFile configFile (pkgConfigFileContents name) -- write example main module if none exists let mainFile := dir / mainFileName name diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean index 579f275fa2..4b6c07515f 100644 --- a/Lake/LeanConfig.lean +++ b/Lake/LeanConfig.lean @@ -12,7 +12,9 @@ namespace Lake def pkgModName : Name := `package def pkgDefName : Name := `package -def pkgFileName : FilePath := "package.lean" + +/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/ +def defaultConfigFile : FilePath := "lakefile.lean" namespace Package @@ -41,8 +43,8 @@ unsafe def fromLeanFileUnsafe constant fromLeanFile (path : FilePath) (dir : FilePath) (args : List String := []) : IO Package unsafe def fromDirUnsafe -(dir : FilePath) (args : List String := []) (file := pkgFileName) : IO Package := +(dir : FilePath) (args : List String := []) (file := defaultConfigFile) : IO Package := fromLeanFileUnsafe (dir / file) dir args @[implementedBy fromDirUnsafe] -constant fromDir (dir : FilePath) (args : List String := []) (file := pkgFileName) : IO Package +constant fromDir (dir : FilePath) (args : List String := []) (file := defaultConfigFile) : IO Package diff --git a/Lake/Package.lean b/Lake/Package.lean index a3d0dba209..5f9f497d5b 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -51,7 +51,7 @@ def defaultDepsDir : FilePath := "lean_packages" -/ inductive Source where | path (dir : FilePath) : Source -| git (url rev : String) (branch : Option String) : Source +| git (url rev : String) (branch : Option String := none) : Source deriving Inhabited, Repr /-- A `Dependency` of a package. -/ diff --git a/README.md b/README.md index 25ec0d32af..ec4c705c4f 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # Lake Lake (Lean Make) is a new build system and package manager for Lean 4. -With Lake, package configuration is written in Lean inside a dedicated `package.lean` file stored in the root of the package directory. Each `package.lean` includes a `package` declaration (akin to `main`) which defines the package's configuration. +With Lake, package configuration is written in Lean inside a dedicated `lakefile.lean` stored in the root of the package directory. Each `lakefile.lean` includes a `package` declaration (akin to `main`) which defines the package's configuration. ## Building and Running Lake @@ -40,7 +40,7 @@ def main : IO Unit := IO.println "Hello, world!" ``` -Lake also creates a basic `package.lean` for the package: +Lake also creates a basic `lakefile.lean` for the package: ```lean import Lake diff --git a/examples/bootstrap/package.lean b/examples/bootstrap/lakefile.lean similarity index 100% rename from examples/bootstrap/package.lean rename to examples/bootstrap/lakefile.lean diff --git a/examples/deps/a/package.lean b/examples/deps/a/lakefile.lean similarity index 100% rename from examples/deps/a/package.lean rename to examples/deps/a/lakefile.lean diff --git a/examples/deps/b/package.lean b/examples/deps/b/lakefile.lean similarity index 100% rename from examples/deps/b/package.lean rename to examples/deps/b/lakefile.lean diff --git a/examples/deps/foo/package.lean b/examples/deps/foo/lakefile.lean similarity index 100% rename from examples/deps/foo/package.lean rename to examples/deps/foo/lakefile.lean diff --git a/examples/ffi-dep/package.lean b/examples/ffi-dep/lakefile.lean similarity index 100% rename from examples/ffi-dep/package.lean rename to examples/ffi-dep/lakefile.lean diff --git a/examples/ffi/package.lean b/examples/ffi/lakefile.lean similarity index 100% rename from examples/ffi/package.lean rename to examples/ffi/lakefile.lean diff --git a/examples/git/package.lean b/examples/git/lakefile.lean similarity index 61% rename from examples/git/package.lean rename to examples/git/lakefile.lean index 40cbf0790a..d1ad7467e0 100644 --- a/examples/git/package.lean +++ b/examples/git/lakefile.lean @@ -7,9 +7,7 @@ package where { name := "hello", src := Source.git - "https://github.com/tydeu/lean4-lake.git" - "7a230da4073dd979ca521e81dcacdacd930c36d4" - (branch := none) + "https://github.com/tydeu/lean4-lake.git" "master" dir := FilePath.mk "examples" / "hello" } ] diff --git a/examples/hello/package.lean b/examples/hello/lakefile.lean similarity index 100% rename from examples/hello/package.lean rename to examples/hello/lakefile.lean diff --git a/examples/io/package.lean b/examples/io/lakefile.lean similarity index 100% rename from examples/io/package.lean rename to examples/io/lakefile.lean diff --git a/examples/main/package.lean b/examples/main/lakefile.lean similarity index 100% rename from examples/main/package.lean rename to examples/main/lakefile.lean