From cb0eab4cbcfe58090b3c739e1e90982804597704 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 25 May 2022 16:52:41 -0400
Subject: [PATCH] refactor: cleanup `runFrontend`

---
 Lake/CLI/Main.lean    |  2 +-
 Lake/Config/Load.lean | 38 +++++++++++++++++++++-----------------
 2 files changed, 22 insertions(+), 18 deletions(-)

diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index a52b37a..d00b620 100644
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@@ -92,7 +92,7 @@ def getLakeInstall? : CliStateM (Option LakeInstall) :=
 def loadPkg (args : List String := []) : CliStateM Package := do
   let dir ← getRootDir; let file ← getConfigFile
   setupLeanSearchPath (← getLeanInstall?) (← getLakeInstall?)
-  Package.load dir args (dir / file)
+  Package.load dir args (dir / file) |>.run LogMethods.eio (m := IO)
 
 def loadWorkspace (args : List String := []) (updateDeps := false) : CliStateM Workspace := do
   let pkg ← loadPkg args
diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean
index aeddd67..6eeb17a 100644
--- a/Lake/Config/Load.lean
+++ b/Lake/Config/Load.lean
@@ -47,39 +47,43 @@ deriving instance BEq, Hashable for Import
 initialize importEnvCache : IO.Ref (Std.HashMap (List Import) Environment) ← IO.mkRef {}
 
 /-- Like `Lean.Elab.processHeader`, but using `importEnvCache`. -/
-def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32)
-: IO (Environment × MessageLog) := do
+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, messages)
-    let env ← importModules imports {} trustLevel
+    if let some env := (← importEnvCache.get).find? imports then
+      return env
+    let env ← importModules imports opts trustLevel
     importEnvCache.modify (·.insert imports env)
-    return (env, messages)
+    return env
   catch e =>
-    let env ← mkEmptyEnvironment
-    let spos := header.getPos?.getD 0
-    let pos  := inputCtx.fileMap.toPosition spos
-    return (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos })
+    let pos := inputCtx.fileMap.toPosition <| header.getPos?.getD 0
+    modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
+    mkEmptyEnvironment
 
 /-- Like `Lean.Elab.runFrontend`, but using `importEnvCache`. -/
-def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 1024)
-: IO (Environment × Bool) := do
+def runFrontend (input : String) (opts : Options)
+(fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 1024)
+: LogT IO (Environment × Bool) := do
   let inputCtx := Parser.mkInputContext input fileName
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
-  let (env, messages) ← processHeader header messages inputCtx trustLevel
+  let (env, messages) ← processHeader header opts trustLevel inputCtx messages
   let env := env.setMainModule mainModuleName
 
-  let mut commandState := Elab.Command.mkState env {} opts
+  let mut commandState := Elab.Command.mkState env messages opts
   let s ← Elab.IO.processCommands inputCtx parserState commandState
   for msg in s.commandState.messages.toList do
-    IO.eprint (← msg.toString)
+    match msg.severity with
+    | MessageSeverity.information => logInfo (← msg.toString)
+    | MessageSeverity.warning     => logWarning (← msg.toString)
+    | MessageSeverity.error       => logError (← msg.toString)
 
-  pure (s.commandState.env, !s.commandState.messages.hasErrors)
+  return (s.commandState.env, !s.commandState.messages.hasErrors)
 
 /-- Unsafe implementation of `load`. -/
 unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty)
-: IO Package := do
+: LogT IO Package := do
   let input ← IO.FS.readFile configFile
   let (env, ok) ← runFrontend input leanOpts configFile.toString configModName
   if ok then
@@ -100,4 +104,4 @@ 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
+(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogT IO Package