From aaf3c1e959d936aa7f6fbbf99be215f3dc113459 Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 15 Jul 2022 21:42:20 -0400 Subject: [PATCH] refactor: split config elab into its own file --- Lake/Load/Elab.lean | 67 ++++++++++++++++++++++++++++++++++++++++++ Lake/Load/Package.lean | 55 ++-------------------------------- 2 files changed, 69 insertions(+), 53 deletions(-) create mode 100644 Lake/Load/Elab.lean diff --git a/Lake/Load/Elab.lean b/Lake/Load/Elab.lean new file mode 100644 index 0000000000..5bc440a82d --- /dev/null +++ b/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 diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean index 72180c4fb7..19008078ad 100644 --- a/Lake/Load/Package.lean +++ b/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)