refactor: split config elab into its own file

Lake/Load/Elab.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Elab.Frontend
+import Lake.DSL.Extensions
+import Lake.Load.Config
+import Lake.Util.Log
+
+namespace Lake
+open Lean System
+
+deriving instance BEq, Hashable for Import
+
+/- Cache for the imported header environment of Lake configuration files. -/
+initialize importEnvCache : IO.Ref (Std.HashMap (List Import) Environment) ← IO.mkRef {}
+
+/-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
+def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
+(inputCtx : Parser.InputContext) : StateT MessageLog IO Environment := do
+  try
+    let imports := Elab.headerToImports header
+    if let some env := (← importEnvCache.get).find? imports then
+      return env
+    let env ← importModules imports opts trustLevel
+    importEnvCache.modify (·.insert imports env)
+    return env
+  catch e =>
+    let pos := inputCtx.fileMap.toPosition <| header.getPos?.getD 0
+    modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
+    mkEmptyEnvironment
+
+/-- Main module `Name` of a Lake configuration file. -/
+def configModuleName : Name := `lakefile
+
+/-- Elaborate `configFile` with the given package directory and options. -/
+def elabConfigFile (pkgDir : FilePath) (configOpts : NameMap String)
+(configFile := pkgDir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Environment := do
+
+  -- Read file and initialize environment
+  let input ← IO.FS.readFile configFile
+  let inputCtx := Parser.mkInputContext input configFile.toString
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, messages) ← processHeader header leanOpts 1024 inputCtx messages
+  let env := env.setMainModule configModuleName
+
+  -- Configure extensions
+  let env := dirExt.setState env pkgDir
+  let env := optsExt.setState env configOpts
+
+  -- Elaborate File
+  let commandState := Elab.Command.mkState env messages leanOpts
+  let s ← Elab.IO.processCommands inputCtx parserState commandState
+
+  -- Log messages
+  for msg in s.commandState.messages.toList do
+    match msg.severity with
+    | MessageSeverity.information => logInfo (← msg.toString)
+    | MessageSeverity.warning     => logWarning (← msg.toString)
+    | MessageSeverity.error       => logError (← msg.toString)
+
+  -- Check result
+  if s.commandState.messages.hasErrors then
+    error s!"{configFile}: package configuration has errors"
+  else
+    return s.commandState.env

Lake/Load/Package.lean

@@ -3,39 +3,14 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean.Elab.Frontend
 import Lake.DSL.Attributes
-import Lake.DSL.Extensions
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
-import Lake.Load.Config
+import Lake.Load.Elab
 
 namespace Lake
 open Lean System
 
-/-- Main module `Name` of a Lake configuration file. -/
-def configModuleName : Name := `lakefile
-
-deriving instance BEq, Hashable for Import
-
-/- Cache for the imported header environment of Lake configuration files. -/
-initialize importEnvCache : IO.Ref (Std.HashMap (List Import) Environment) ← IO.mkRef {}
-
-/-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
-def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
-(inputCtx : Parser.InputContext) : StateT MessageLog IO Environment := do
-  try
-    let imports := Elab.headerToImports header
-    if let some env := (← importEnvCache.get).find? imports then
-      return env
-    let env ← importModules imports opts trustLevel
-    importEnvCache.modify (·.insert imports env)
-    return env
-  catch e =>
-    let pos := inputCtx.fileMap.toPosition <| header.getPos?.getD 0
-    modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
-    mkEmptyEnvironment
-
 /-- Like `Lean.Environment.evalConstCheck` but with plain universe-polymorphic `Except`. -/
 unsafe def evalConstCheck (env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α :=
   match env.find? const with
@@ -144,30 +119,4 @@ the given directory with the given configuration file.
 -/
 def Package.load (dir : FilePath) (configOpts : NameMap String)
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package := do
-
-  -- Read file and initialize environment
-  let input ← IO.FS.readFile configFile
-  let inputCtx := Parser.mkInputContext input configFile.toString
-  let (header, parserState, messages) ← Parser.parseHeader inputCtx
-  let (env, messages) ← processHeader header leanOpts 1024 inputCtx messages
-  let env := env.setMainModule configModuleName
-
-  -- Configure extensions
-  let env := dirExt.setState env dir
-  let env := optsExt.setState env configOpts
-
-  -- Elaborate File
-  let commandState := Elab.Command.mkState env messages leanOpts
-  let s ← Elab.IO.processCommands inputCtx parserState commandState
-
-  -- Report errors
-  for msg in s.commandState.messages.toList do
-    match msg.severity with
-    | MessageSeverity.information => logInfo (← msg.toString)
-    | MessageSeverity.warning     => logWarning (← msg.toString)
-    | MessageSeverity.error       => logError (← msg.toString)
-  if s.commandState.messages.hasErrors then
-    error s!"package configuration `{configFile}` has errors"
-
-  -- Load package from the environment
-  Package.loadFromEnv s.commandState.env
+  Package.loadFromEnv (← elabConfigFile dir configOpts configFile leanOpts)