From 68f0eb16bdec8f9e3fc448d8aa12502aeda3b373 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 8 Jun 2021 17:18:27 -0400 Subject: [PATCH] Minor LeanConfig code cleanup --- Lake/LeanConfig.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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