feat: __dir__/`__args__ syntax for config settings

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,32 +62,34 @@ 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
     | MessageSeverity.information => logInfo (← msg.toString)
     | 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] =>

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

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?

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)

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__]
 }

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}