refactor: simplify / reorder LeanConfig

Lake/Cli.lean

@@ -64,7 +64,7 @@ def setWantsHelp : CliM PUnit :=
   modifyThe CliOptions fun st => {st with wantsHelp := true}
 
 def loadPkg (args : List String) : CliM Package := do
-  Package.fromDir (← getDir) args (← getFile)
+  let dir ← getDir; let file ← getFile; Package.load dir args (dir / file)
 
 def takeArg : CliM String := do
   match (← takeArg?) with

Lake/LeanConfig.lean

@@ -7,52 +7,58 @@ import Lean
 import Lake.Package
 import Lake.Attributes
 
+namespace Lake
 open Lean System
 
-namespace Lake
-
+/-- Main module `Name` of a Lake configuration file. -/
 def configModName : Name := `lakefile
 
 /-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
 def defaultConfigFile : FilePath := "lakefile.lean"
 
+/-- Evaluate a `package` declaration to its respective `PackageConfig`. -/
+unsafe def evalPackageDecl (env : Environment) (declName : Name)
+(dir : FilePath) (args : List String := []) (leanOpts := Options.empty)
+: IO PackageConfig := do
+  let m := env.evalConstCheck IOPackager leanOpts ``IOPackager declName
+  if let Except.ok ioPackager := m.run.run then
+    return ← ioPackager dir args
+  let m := env.evalConstCheck Packager leanOpts ``Packager declName
+  if let Except.ok packager := m.run.run then
+    return packager dir args
+  let m := env.evalConstCheck PackageConfig leanOpts ``PackageConfig declName
+  if let Except.ok config := m.run.run then
+    return config
+  throw <| IO.userError <|
+    s!"unexpected type at `{declName}`, " ++
+      "`Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected"
+
 namespace Package
 
-unsafe def fromLeanFileUnsafe
-(path : FilePath) (dir : FilePath) (args : List String := [])
+/-- Unsafe implementation of `load`. -/
+unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
+(configFile := dir / defaultConfigFile) (leanOpts := Options.empty)
 : IO Package := do
-  let opts := Options.empty
-  let input ← IO.FS.readFile path
-  let (env, ok) ← Elab.runFrontend input opts path.toString configModName
+  let input ← IO.FS.readFile configFile
+  let (env, ok) ← Elab.runFrontend input leanOpts configFile.toString configModName
   if ok then
     match packageAttr.ext.getState env |>.toList with
     | [] =>
       throw <| IO.userError
         s!"configuration file is missing a `package` declaration"
     | [pkgDeclName] =>
-      let m := env.evalConstCheck IOPackager opts ``IOPackager pkgDeclName
-      if let Except.ok ioPackager := m.run.run then
-        return Package.mk dir (← ioPackager dir args)
-      let m := env.evalConstCheck Packager opts ``Packager pkgDeclName
-      if let Except.ok packager := m.run.run then
-        return Package.mk dir (packager dir args)
-      let m := env.evalConstCheck PackageConfig opts ``PackageConfig pkgDeclName
-      if let Except.ok config := m.run.run then
-        return Package.mk dir config
-      throw <| IO.userError
-        s!"unexpected type at 'package', `Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected"
+      let config ← evalPackageDecl env pkgDeclName dir args leanOpts
+      return Package.mk dir config
     | _ =>
       throw <| IO.userError
         s!"configuration file has multiple `package` declarations"
   else
-    throw <| IO.userError s!"package configuration (at {path}) has errors"
+    throw <| IO.userError s!"package configuration `{configFile}` has errors"
 
-@[implementedBy fromLeanFileUnsafe]
-constant fromLeanFile (path : FilePath) (dir : FilePath) (args : List String := []) : IO Package
-
-unsafe def fromDirUnsafe
-(dir : FilePath) (args : List String := []) (file := defaultConfigFile) : IO Package :=
-  fromLeanFileUnsafe (dir / file) dir args
-
-@[implementedBy fromDirUnsafe]
-constant fromDir (dir : FilePath) (args : List String := []) (file := defaultConfigFile) : IO Package
+/--
+  Load the package located in
+  the given directory with the given configuration file.
+-/
+@[implementedBy loadUnsafe]
+constant load (dir : FilePath) (args : List String := [])
+(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : IO Package

Lake/Resolve.lean

@@ -51,7 +51,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
+  let depPkg ← Package.load (dir / dep.dir) dep.args
   unless depPkg.name == dep.name do
     throw <| IO.userError <|
       s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++