diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index 8161dce..6d0ca76 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -12,7 +12,7 @@ namespace Lake open Lean System /-- Main module `Name` of a Lake configuration file. -/ -def configModName : Name := `lakefile +def configModuleName : Name := `lakefile /-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/ def defaultConfigFile : FilePath := "lakefile.lean" @@ -62,16 +62,24 @@ def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32) modify (·.add { fileName := inputCtx.fileName, data := toString e, pos }) mkEmptyEnvironment -/-- Like `Lean.Elab.runFrontend`, but using `importEnvCache`. -/ -def runFrontend (input : String) (opts : Options) -(fileName : String) (mainModuleName : Name) (trustLevel : UInt32 := 1024) -: LogT IO (Environment × Bool) := do - let inputCtx := Parser.mkInputContext input fileName +/-- Unsafe implementation of `load`. -/ +unsafe def loadUnsafe (dir : FilePath) (args : List String := []) +(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) +: LogT IO Package := do + + -- Read File & Initialize Environment + let input ← IO.FS.readFile configFile + let inputCtx := Parser.mkInputContext input configFile.toString let (header, parserState, messages) ← Parser.parseHeader inputCtx - let (env, messages) ← processHeader header opts trustLevel inputCtx messages - let env := env.setMainModule mainModuleName + let (env, messages) ← processHeader header leanOpts 1024 inputCtx messages + let env := env.setMainModule configModuleName + + -- Configure Extensions + let env := dirExt.setState env dir + let env := argsExt.setState env args - let mut commandState := Elab.Command.mkState env messages opts + -- Elaborate File + let commandState := Elab.Command.mkState env messages leanOpts let s ← Elab.IO.processCommands inputCtx parserState commandState for msg in s.commandState.messages.toList do match msg.severity with @@ -79,15 +87,9 @@ def runFrontend (input : String) (opts : Options) | MessageSeverity.warning => logWarning (← msg.toString) | MessageSeverity.error => logError (← msg.toString) - return (s.commandState.env, !s.commandState.messages.hasErrors) - -/-- Unsafe implementation of `load`. -/ -unsafe def loadUnsafe (dir : FilePath) (args : List String := []) -(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) -: LogT IO Package := do - let input ← IO.FS.readFile configFile - let (env, ok) ← runFrontend input leanOpts configFile.toString configModName - if ok then + -- Extract Configuration + let env := s.commandState.env + if !s.commandState.messages.hasErrors then match packageAttr.ext.getState env |>.toList with | [] => error s!"configuration file is missing a `package` declaration" | [pkgDeclName] => diff --git a/Lake/DSL.lean b/Lake/DSL.lean index 1896ea7..8cc6786 100644 --- a/Lake/DSL.lean +++ b/Lake/DSL.lean @@ -4,5 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.DSL.Attributes +import Lake.DSL.Extensions import Lake.DSL.Commands import Lake.DSL.Require +import Lake.DSL.Config diff --git a/Lake/DSL/Config.lean b/Lake/DSL/Config.lean new file mode 100644 index 0000000..2390363 --- /dev/null +++ b/Lake/DSL/Config.lean @@ -0,0 +1,49 @@ +/- +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.Elab.ElabRules +import Lake.DSL.Extensions + +namespace Lake.DSL +open Lean Elab Term + +/-- +A dummy default constant for `__dir__` to make it type check +outside Lakefile elaboration (e.g., when editing). +-/ +constant dummyDir : System.FilePath + +/-- +A dummy default constant for `__args__` to make it type check +outside Lakefile elaboration (e.g., when editing). +-/ +constant dummyArgs : List String + +/-- +A macro that expands to the path of package's directory +during the Lakefile's elaboration. +-/ +scoped elab stx:"__dir__" : term <= expectedType? => do + let exp := + if let some dir := dirExt.getState (← getEnv) then + let str := Syntax.mkStrLit dir.toString (SourceInfo.fromRef stx) + Syntax.mkApp (mkCIdentFrom stx ``System.FilePath.mk) #[str] + else + -- `id` app forces Lean to show macro's doc rather than the constant's + Syntax.mkApp (mkCIdentFrom stx ``id) #[mkCIdentFrom stx ``dummyDir] + withMacroExpansion stx exp <| elabTerm exp expectedType? + +/-- +A macro that expands to the configuration arguments passed +via the Lake command line during the Lakefile's elaboration. +-/ +scoped elab stx:"__args__" : term <= expectedType? => do + let exp := + if let some args := argsExt.getState (← getEnv) then + quote args + else + -- `id` app forces Lean to show macro's doc rather than the constant's + Syntax.mkApp (mkCIdentFrom stx ``id) #[mkCIdentFrom stx ``dummyArgs] + withMacroExpansion stx exp <| elabTerm exp expectedType? diff --git a/Lake/DSL/Extensions.lean b/Lake/DSL/Extensions.lean index 1e51ef2..f1ab0cf 100644 --- a/Lake/DSL/Extensions.lean +++ b/Lake/DSL/Extensions.lean @@ -12,3 +12,9 @@ namespace Lake initialize depsExt : EnvExtension (Array Dependency) ← registerEnvExtension (pure #[]) + +initialize dirExt : EnvExtension (Option System.FilePath) ← + registerEnvExtension (pure none) + +initialize argsExt : EnvExtension (Option (List String)) ← + registerEnvExtension (pure none) diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean index 1d45d7e..8e6b0bd 100644 --- a/examples/ffi/lib/lakefile.lean +++ b/examples/ffi/lib/lakefile.lean @@ -15,10 +15,10 @@ def cLibTarget (pkgDir : FilePath) : FileTarget := let libFile := pkgDir / buildDir / cDir / "libffi.a" staticLibTarget libFile #[ffiOTarget pkgDir] -package ffi (pkgDir) (args) { +package ffi { -- customize layout srcDir := "lean" libRoots := #[`Ffi] -- specify the lib as an additional target - moreLibTargets := #[cLibTarget pkgDir] + moreLibTargets := #[cLibTarget __dir__] } diff --git a/examples/io/lakefile.lean b/examples/io/lakefile.lean index 7213774..c2ad51a 100644 --- a/examples/io/lakefile.lean +++ b/examples/io/lakefile.lean @@ -1,6 +1,9 @@ import Lake open Lake DSL +#eval show IO _ from do + IO.println s!"elaborating configuration in {__dir__} with args {__args__}" + package io (dir) (args) do IO.println s!"computing io package in {dir} with args {args} ..." return {name := `io}