refactor: rename package.lean to lakefile.lean

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)

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

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

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

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

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"
     }
   ]