max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: use error in Load.lean

Browse source
This commit is contained in:
tydeu 2021-12-11 17:53:31 -05:00
parent 197b8e5c1d
commit 8b66dbf285
1 changed files with 5 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
Lake/Config/Load.lean
View file

@ -29,9 +29,8 @@ unsafe def evalPackageDecl (env : Environment) (declName : Name)
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"
error <| s!"unexpected type at `{declName}`, " ++
"`Lake.IOPackager`, `Lake.Packager`, or `Lake.PackageConfig` expected"
/-- Evaluate a `script` declaration to its respective `Script`. -/
unsafe def evalScriptDecl
@ -50,19 +49,15 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
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"
| [] => error s!"configuration file is missing a `package` declaration"
| [pkgDeclName] =>
let config ← evalPackageDecl env pkgDeclName dir args leanOpts
let scripts ← scriptAttr.ext.getState env |>.foldM (init := {})
fun m d => do m.insert d <| ← evalScriptDecl env d leanOpts
return {dir, config, scripts}
| _ =>
throw <| IO.userError
s!"configuration file has multiple `package` declarations"
| _ => error s!"configuration file has multiple `package` declarations"
else
throw <| IO.userError s!"package configuration `{configFile}` has errors"
error s!"package configuration `{configFile}` has errors"
/--
Load the package located in