diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean index f0270f55ee..6fece98b92 100644 --- a/Lake/LeanConfig.lean +++ b/Lake/LeanConfig.lean @@ -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