@@ -37,7 +37,7 @@ def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
3737 mkEmptyEnvironment
3838
3939/-- Like `Lean.Environment.evalConstCheck` but with plain universe-polymorphic `Except`. -/
40- unsafe def evalConstCheck (α) ( env : Environment) (opts : Options) (type : Name) (const : Name) : Except String α :=
40+ unsafe def evalConstCheck (env : Environment) (opts : Options) (α ) (type : Name) (const : Name) : Except String α :=
4141 match env.find? const with
4242 | none => throw s! "unknown constant '{ const} '"
4343 | some info =>
@@ -52,115 +52,122 @@ where
5252 throwUnexpectedType : Except String α :=
5353 throw s! "unexpected type at '{ const} ', `{ type} ` expected"
5454
55- namespace Package
56-
57- /-- Unsafe implementation of `load`. -/
58- unsafe def loadUnsafe (dir : FilePath) (configOpts : NameMap String)
59- (configFile := dir / defaultConfigFile) (leanOpts := Options.empty)
60- : LogIO Package := do
61-
62- -- Read File & Initialize Environment
63- let input ← IO.FS.readFile configFile
64- let inputCtx := Parser.mkInputContext input configFile.toString
65- let (header, parserState, messages) ← Parser.parseHeader inputCtx
66- let (env, messages) ← processHeader header leanOpts 1024 inputCtx messages
67- let env := env.setMainModule configModuleName
68-
69- -- Configure Extensions
70- let env := dirExt.setState env dir
71- let env := optsExt.setState env configOpts
72-
73- -- Elaborate File
74- let commandState := Elab.Command.mkState env messages leanOpts
75- let s ← Elab.IO.processCommands inputCtx parserState commandState
76- for msg in s.commandState.messages.toList do
77- match msg.severity with
78- | MessageSeverity.information => logInfo (← msg.toString)
79- | MessageSeverity.warning => logWarning (← msg.toString)
80- | MessageSeverity.error => logError (← msg.toString)
81-
82- -- Extract Configuration
83- if s.commandState.messages.hasErrors then
84- error s! "package configuration `{ configFile} ` has errors"
85-
86- -- Load Package Configuration
87- let env := s.commandState.env
55+ /-- Construct a `NameMap` from the declarations tagged with `attr`. -/
56+ def mkTagMap
57+ (env : Environment) (attr : TagAttribute)
58+ [Monad m] (f : Name → m α) : m (NameMap α) :=
59+ attr.ext.getState env |>.foldM (init := {}) fun map declName =>
60+ return map.insert declName <| ← f declName
61+
62+ /-- Construct a `DNameMap` from the declarations tagged with `attr`. -/
63+ def mkDTagMap
64+ (env : Environment) (attr : TagAttribute)
65+ [Monad m] (f : (n : Name) → m (β n)) : m (DNameMap β) :=
66+ attr.ext.getState env |>.foldM (init := {}) fun map declName =>
67+ return map.insert declName <| ← f declName
68+
69+ /-- Unsafe implementation of `loadFromEnv`. -/
70+ unsafe def Package.unsafeLoadFromEnv
71+ (env : Environment) (leanOpts := Options.empty) : LogIO Package := do
72+
73+ -- Load Configuration
8874 let pkgDeclName ←
8975 match packageAttr.ext.getState env |>.toList with
9076 | [] => error s! "configuration file is missing a `package` declaration"
9177 | [name] => pure name
9278 | _ => error s! "configuration file has multiple `package` declarations"
9379 let config ← IO.ofExcept <|
94- evalConstCheck PackageConfig env leanOpts ``PackageConfig pkgDeclName
95- if config.extraDepTarget.isSome then
96- logWarning <| "`extraDepTarget` has been deprecated. " ++
97- "Try to use a custom target or raise an issue about your use case."
80+ evalConstCheck env leanOpts PackageConfig ``PackageConfig pkgDeclName
9881
99- -- Tag Load Helpers
100- let mkTagMap {α} (attr) (f : Name → IO α) : IO (NameMap α) :=
101- attr.ext.getState env |>.foldM (init := {}) fun map declName =>
102- return map.insert declName <| ← f declName
103- let mkDTagMap {β} (attr : TagAttribute) (f : (n : Name) → IO (β n)) : IO (DNameMap β) :=
104- attr.ext.getState env |>.foldM (init := {}) fun map declName =>
105- return map.insert declName <| ← f declName
106- let evalConst (α typeName declName) : IO α :=
107- IO.ofExcept (evalConstCheck α env leanOpts typeName declName)
108- let evalConstMap {α β} (f : α → β) (declName) : IO β :=
109- match env.evalConst α leanOpts declName with
110- | .ok a => pure <| f a
111- | .error e => throw <| IO.userError e
112-
113- -- Load Dependency, Script, Facet, & Target Configurations
114- let dependencies ←
82+ -- Load Dependencies
83+ let dependencies ← IO.ofExcept <|
11584 packageDepAttr.ext.getState env |>.foldM (init := #[]) fun arr name => do
116- return arr.push <| ← evalConst Dependency ``Dependency name
117- let scripts ← mkTagMap scriptAttr fun declName => do
118- let fn ← IO.ofExcept <| evalConstCheck ScriptFn env leanOpts ``ScriptFn declName
119- return {fn, doc? := (← findDocString? env declName)}
120- let leanLibConfigs ← mkTagMap leanLibAttr
121- (evalConst LeanLibConfig ``LeanLibConfig)
122- let leanExeConfigs ← mkTagMap leanExeAttr
123- (evalConst LeanExeConfig ``LeanExeConfig)
124- let externLibConfigs ← mkTagMap externLibAttr
125- (evalConst ExternLibConfig ``ExternLibConfig)
126- let opaqueModuleFacetConfigs ← mkDTagMap moduleFacetAttr fun name => do
127- match evalConstCheck ModuleFacetDecl env leanOpts ``ModuleFacetDecl name with
85+ return arr.push <| ← evalConstCheck env leanOpts Dependency ``Dependency name
86+
87+ -- Load Script, Facet, & Target Configurations
88+ let scripts ← mkTagMap env scriptAttr fun name => do
89+ let fn ← IO.ofExcept <| evalConstCheck env leanOpts ScriptFn ``ScriptFn name
90+ return {fn, doc? := (← findDocString? env name)}
91+ let leanLibConfigs ← IO.ofExcept <| mkTagMap env leanLibAttr fun name =>
92+ evalConstCheck env leanOpts LeanLibConfig ``LeanLibConfig name
93+ let leanExeConfigs ← IO.ofExcept <| mkTagMap env leanExeAttr fun name =>
94+ evalConstCheck env leanOpts LeanExeConfig ``LeanExeConfig name
95+ let externLibConfigs ← IO.ofExcept <| mkTagMap env externLibAttr fun name =>
96+ evalConstCheck env leanOpts ExternLibConfig ``ExternLibConfig name
97+ let opaqueModuleFacetConfigs ← mkDTagMap env moduleFacetAttr fun name => do
98+ match evalConstCheck env leanOpts ModuleFacetDecl ``ModuleFacetDecl name with
12899 | .ok decl =>
129100 if h : name = decl.name then
130101 return OpaqueModuleFacetConfig.mk (h ▸ decl.config)
131102 else
132- error s! "Facet was defined as `{ decl.name} `, but was registered as `{ name} `"
103+ error s! "facet was defined as `{ decl.name} `, but was registered as `{ name} `"
133104 | .error e => throw <| IO.userError e
134- let opaquePackageFacetConfigs ← mkDTagMap packageFacetAttr fun name => do
135- match evalConstCheck PackageFacetDecl env leanOpts ``PackageFacetDecl name with
105+ let opaquePackageFacetConfigs ← mkDTagMap env packageFacetAttr fun name => do
106+ match evalConstCheck env leanOpts PackageFacetDecl ``PackageFacetDecl name with
136107 | .ok decl =>
137108 if h : name = decl.name then
138109 return OpaquePackageFacetConfig.mk (h ▸ decl.config)
139110 else
140- error s! "Facet was defined as `{ decl.name} `, but was registered as `{ name} `"
111+ error s! "facet was defined as `{ decl.name} `, but was registered as `{ name} `"
112+ | .error e => throw <| IO.userError e
113+ let opaqueTargetConfigs ← mkTagMap env targetAttr fun declName =>
114+ match evalConstCheck env leanOpts TargetConfig ``TargetConfig declName with
115+ | .ok a => pure <| OpaqueTargetConfig.mk a
141116 | .error e => throw <| IO.userError e
142- let opaqueTargetConfigs ← mkTagMap targetAttr
143- (evalConstMap OpaqueTargetConfig.mk)
144- let defaultTargets :=
145- defaultTargetAttr.ext.getState env |>.fold (init := #[]) fun arr name =>
146- arr.push name
117+ let defaultTargets := defaultTargetAttr.ext.getState env |>.fold (·.push ·) #[]
147118
148- -- Construct the Package
119+ -- Issue Warnings
120+ if config.extraDepTarget.isSome then
121+ logWarning <| "`extraDepTarget` has been deprecated. " ++
122+ "Try to use a custom target or raise an issue about your use case."
149123 if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then
150124 logWarning <| "Package targets are deprecated. " ++
151125 "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
126+
127+ -- Construct the Package
128+ let some dir := dirExt.getState env
129+ | error "configuration environment has no package directory set"
152130 return {
153131 dir, config, scripts, dependencies,
154132 leanLibConfigs, leanExeConfigs, externLibConfigs,
155133 opaqueModuleFacetConfigs, opaquePackageFacetConfigs, opaqueTargetConfigs,
156134 defaultTargets
157135 }
158136
137+ /-- Load a `Package` from a configuration environment. -/
138+ @[implementedBy unsafeLoadFromEnv] opaque Package.loadFromEnv
139+ (env : Environment) (leanOpts := Options.empty) : LogIO Package
159140
160141/--
161- Load the package located in
142+ Load the `Package` located in
162143the given directory with the given configuration file.
163144-/
164- @[implementedBy loadUnsafe]
165- opaque load (dir : FilePath) (configOpts : NameMap String)
166- (configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package
145+ def Package.load (dir : FilePath) (configOpts : NameMap String)
146+ (configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package := do
147+
148+ -- Read file and initialize environment
149+ let input ← IO.FS.readFile configFile
150+ let inputCtx := Parser.mkInputContext input configFile.toString
151+ let (header, parserState, messages) ← Parser.parseHeader inputCtx
152+ let (env, messages) ← processHeader header leanOpts 1024 inputCtx messages
153+ let env := env.setMainModule configModuleName
154+
155+ -- Configure extensions
156+ let env := dirExt.setState env dir
157+ let env := optsExt.setState env configOpts
158+
159+ -- Elaborate File
160+ let commandState := Elab.Command.mkState env messages leanOpts
161+ let s ← Elab.IO.processCommands inputCtx parserState commandState
162+
163+ -- Report errors
164+ for msg in s.commandState.messages.toList do
165+ match msg.severity with
166+ | MessageSeverity.information => logInfo (← msg.toString)
167+ | MessageSeverity.warning => logWarning (← msg.toString)
168+ | MessageSeverity.error => logError (← msg.toString)
169+ if s.commandState.messages.hasErrors then
170+ error s! "package configuration `{ configFile} ` has errors"
171+
172+ -- Load package from the environment
173+ Package.loadFromEnv s.commandState.env
0 commit comments