Minor LeanConfig code cleanup

This commit is contained in:
Mac Malone 2021-06-08 17:18:27 -04:00
parent 6fad405294
commit 68f0eb16bd

View file

@ -1,13 +1,12 @@
/-
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
import Lean.Elab.Frontend
import Lake.Package
open Lean Elab System
open Lean System
namespace Lake
@ -17,7 +16,7 @@ namespace PackageConfig
unsafe def fromLeanFileUnsafe (path : FilePath) : IO PackageConfig := do
let input ← IO.FS.readFile path
let (env, ok) ← runFrontend input Options.empty path.toString `package
let (env, ok) ← Elab.runFrontend input Options.empty path.toString `package
if ok then
IO.ofExcept <| Id.run <| ExceptT.run <|
env.evalConstCheck PackageConfig Options.empty ``PackageConfig `package