chore: lake: builtins for DSL & plugin for server (#7860)

This PR restores the use of builtins (e.g., initializer, elaborators,
and macros) for DSL features and the use of the Lake plugin in the
server.

The motivation is to avoid elaboration breakages in Lake when core types
need changing (e.g., `Environment`).

This reverts #7399 and partially reverts #7608. The use of the plugin is
more narrow -- it is now just used for elaboration of Lake configuration
files in the server. This should hopefully avoid the reappearance of
#7388.

src/lake/Lake/CLI/Serve.lean

@@ -45,6 +45,7 @@ def setupFile
       paths := {
         oleanPath := loadConfig.lakeEnv.leanPath
         srcPath := loadConfig.lakeEnv.leanSrcPath
+        pluginPaths := #[loadConfig.lakeEnv.lake.sharedLib]
       }
       setupOptions := ⟨∅⟩
       : FileSetupInfo

src/lake/Lake/DSL.lean

@@ -14,3 +14,4 @@ import Lake.DSL.Require
 import Lake.DSL.Targets
 import Lake.DSL.Meta
 import Lake.DSL.Key
+import Lake.DSL.VerLit

src/lake/Lake/DSL/Attributes.lean

@@ -10,7 +10,7 @@ open Lean
 
 namespace Lake
 
-initialize
+builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
     name            := `test_runner

src/lake/Lake/DSL/AttributesCore.lean

@@ -9,43 +9,43 @@ import Lake.Util.OrderedTagAttribute
 open Lean
 namespace Lake
 
-initialize packageAttr : OrderedTagAttribute ←
+builtin_initialize packageAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package "mark a definition as a Lake package configuration"
 
-initialize packageDepAttr : OrderedTagAttribute ←
+builtin_initialize packageDepAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
 
-initialize postUpdateAttr : OrderedTagAttribute ←
+builtin_initialize postUpdateAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook"
 
-initialize scriptAttr : OrderedTagAttribute ←
+builtin_initialize scriptAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `script "mark a definition as a Lake script"
 
-initialize defaultScriptAttr : OrderedTagAttribute ←
+builtin_initialize defaultScriptAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `default_script "mark a Lake script as the package's default"
     fun name => do
       unless (← getEnv <&> (scriptAttr.hasTag · name)) do
         throwError "attribute `default_script` can only be used on a `script`"
 
-initialize leanLibAttr : OrderedTagAttribute ←
+builtin_initialize leanLibAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
 
-initialize leanExeAttr : OrderedTagAttribute ←
+builtin_initialize leanExeAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
 
-initialize externLibAttr : OrderedTagAttribute ←
+builtin_initialize externLibAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target"
 
-initialize inputFileAttr : OrderedTagAttribute ←
+builtin_initialize inputFileAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `input_file "mark a definition as a Lake input file target"
 
-initialize inputDirAttr : OrderedTagAttribute ←
+builtin_initialize inputDirAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `input_dir "mark a definition as a Lake input directory target"
 
-initialize targetAttr : OrderedTagAttribute ←
+builtin_initialize targetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `target "mark a definition as a Lake target"
 
-initialize defaultTargetAttr : OrderedTagAttribute ←
+builtin_initialize defaultTargetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `default_target "mark a Lake target as the package's default"
     fun name => do
       let valid ← getEnv <&> fun env =>
@@ -53,7 +53,7 @@ initialize defaultTargetAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
 
-initialize testDriverAttr : OrderedTagAttribute ←
+builtin_initialize testDriverAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `test_driver "mark a Lake script, executable, or library as package's test driver"
     fun name => do
       let valid ← getEnv <&> fun env =>
@@ -63,7 +63,7 @@ initialize testDriverAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `test_driver` can only be used on a `script`, `lean_exe`, or `lean_lib`"
 
-initialize lintDriverAttr : OrderedTagAttribute ←
+builtin_initialize lintDriverAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `lint_driver "mark a Lake script or executable as package's linter"
     fun name => do
       let valid ← getEnv <&> fun env =>
@@ -72,11 +72,11 @@ initialize lintDriverAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `lint_driver` can only be used on a `script` or `lean_exe`"
 
-initialize moduleFacetAttr : OrderedTagAttribute ←
+builtin_initialize moduleFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
 
-initialize packageFacetAttr : OrderedTagAttribute ←
+builtin_initialize packageFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet"
 
-initialize libraryFacetAttr : OrderedTagAttribute ←
+builtin_initialize libraryFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet"

src/lake/Lake/DSL/Config.lean

@@ -28,7 +28,7 @@ during the Lakefile's elaboration.
 -/
 scoped syntax (name := dirConst) "__dir__" : term
 
-@[term_elab dirConst]
+@[builtin_term_elab dirConst]
 def elabDirConst : TermElab := fun stx expectedType? => do
   let exp :=
     if let some dir := dirExt.getState (← getEnv) then
@@ -48,7 +48,7 @@ or via the `with` clause in a `require` statement.
 -/
 scoped syntax (name := getConfig) "get_config? " ident :term
 
-@[term_elab getConfig]
+@[builtin_term_elab getConfig]
 def elabGetConfig : TermElab := fun stx expectedType? => do
   tryPostponeIfNoneOrMVar expectedType?
   match stx with

src/lake/Lake/DSL/Extensions.lean

@@ -10,8 +10,8 @@ open Lean
 
 namespace Lake
 
-initialize dirExt : EnvExtension (Option System.FilePath) ←
+builtin_initialize dirExt : EnvExtension (Option System.FilePath) ←
   registerEnvExtension (pure none)
 
-initialize optsExt : EnvExtension (Option (NameMap String)) ←
+builtin_initialize optsExt : EnvExtension (Option (NameMap String)) ←
   registerEnvExtension (pure none)

src/lake/Lake/DSL/Meta.lean

@@ -57,7 +57,7 @@ extern_lib linuxOnlyLib := ...
 scoped syntax (name := metaIf)
 "meta " "if " term " then " cmdDo (" else " cmdDo)? : command
 
-@[command_elab metaIf]
+@[builtin_command_elab metaIf]
 def elabMetaIf : CommandElab := fun stx => do
   let `(meta if $c then $t $[else $e?]?) := stx
     | throwErrorAt stx "ill-formed meta if command"
@@ -80,7 +80,7 @@ and produces an expression corresponding to the result via `ToExpr α`.
 -/
 scoped syntax:lead (name := runIO) "run_io " doSeq : term
 
-@[term_elab runIO]
+@[builtin_term_elab runIO]
 def elabRunIO : TermElab := fun stx expectedType? =>
   match stx with
   | `(run_io%$tk $t) => withRef t do

src/lake/Lake/DSL/Package.lean

@@ -31,7 +31,7 @@ The defined package configuration will be available for reference as `_package`.
 scoped syntax (name := packageCommand)
 (docComment)? (Term.attributes)? "package " (identOrStr)? optConfig : command
 
-@[command_elab packageCommand]
+@[builtin_command_elab packageCommand]
 def elabPackageCommand : CommandElab := fun stx => do
   let `(packageCommand|$(doc?)? $(attrs?)? package%$kw $[$nameStx?]? $cfg) := stx
     | throwErrorAt stx "ill-formed package declaration"
@@ -80,7 +80,7 @@ optional(docComment) optional(Term.attributes)
 "post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo)
 : command
 
-@[macro postUpdateDecl]
+@[builtin_macro postUpdateDecl]
 def expandPostUpdateDecl : Macro := fun stx => do
   match stx with
   | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) =>

src/lake/Lake/DSL/Require.lean

@@ -143,7 +143,7 @@ options to the dependency on the command line.
 scoped syntax (name := requireDecl)
 (docComment)? "require " depSpec : command
 
-@[macro requireDecl]
+@[builtin_macro requireDecl]
 def expandRequireDecl : Macro := fun stx => do
   let `(requireDecl|$(doc?)? require%$kw $spec) := stx
     | Macro.throwErrorAt stx "ill-formed require declaration"

src/lake/Lake/DSL/Script.lean

@@ -36,7 +36,7 @@ script «script-name» (args) do
 scoped syntax (name := scriptDecl)
 (docComment)?  optional(Term.attributes) "script " scriptDeclSpec : command
 
-@[macro scriptDecl]
+@[builtin_macro scriptDecl]
 def expandScriptDecl : Macro
 | `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? do $seq $[$wds?:whereDecls]?) => do
   `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := do $seq $[$wds?:whereDecls]?)

src/lake/Lake/DSL/Targets.lean

@@ -46,7 +46,7 @@ The `mod` parameter (and its type specifier) is optional.
 scoped syntax (name := moduleFacetDecl)
 (docComment)? (Term.attributes)? "module_facet " buildDeclSig : command
 
-@[macro moduleFacetDecl]
+@[builtin_macro moduleFacetDecl]
 def expandModuleFacetDecl : Macro := fun stx => do
   let `(moduleFacetDecl|$(doc?)? $(attrs?)? module_facet%$kw $sig) := stx
     | Macro.throwErrorAt stx "ill-formed module facet declaration"
@@ -85,7 +85,7 @@ The `pkg` parameter (and its type specifier) is optional.
 scoped syntax (name := packageFacetDecl)
 (docComment)? (Term.attributes)? "package_facet " buildDeclSig : command
 
-@[macro packageFacetDecl]
+@[builtin_macro packageFacetDecl]
 def expandPackageFacetDecl : Macro := fun stx => do
   let `(packageFacetDecl|$(doc?)? $(attrs?)? package_facet%$kw $sig) := stx
     | Macro.throwErrorAt stx "ill-formed package facet declaration"
@@ -124,7 +124,7 @@ The `lib` parameter (and its type specifier) is optional.
 scoped syntax (name := libraryFacetDecl)
 (docComment)? (Term.attributes)? "library_facet " buildDeclSig : command
 
-@[macro libraryFacetDecl]
+@[builtin_macro libraryFacetDecl]
 def expandLibraryFacetDecl : Macro := fun stx => do
   let `(libraryFacetDecl|$(doc?)? $(attrs?)? library_facet%$kw $sig) := stx
     | Macro.throwErrorAt stx "ill-formed library facet declaration"
@@ -172,7 +172,7 @@ provided is the package in which the target is defined.
 scoped syntax (name := targetCommand)
 (docComment)? (Term.attributes)? "target " buildDeclSig : command
 
-@[macro targetCommand]
+@[builtin_macro targetCommand]
 def expandTargetCommand : Macro := fun stx => do
   let `(targetCommand|$(doc?)? $(attrs?)? target%$kw $sig) := stx
     | Macro.throwErrorAt stx "ill-formed target declaration"
@@ -240,7 +240,7 @@ lean_lib «target-name» where /- config opts -/
 scoped syntax (name := leanLibCommand)
 (docComment)? (Term.attributes)? "lean_lib " (identOrStr)? optConfig : command
 
-@[command_elab leanLibCommand]
+@[builtin_command_elab leanLibCommand]
 def elabLeanLibCommand : CommandElab := fun stx => do
   let `(leanLibCommand|$(doc?)? $(attrs?)? lean_lib%$kw $(nameStx?)? $cfg) := stx
     | throwErrorAt stx "ill-formed lean_lib declaration"
@@ -267,7 +267,7 @@ lean_exe «target-name» where /- config opts -/
 scoped syntax (name := leanExeCommand)
 (docComment)? (Term.attributes)? "lean_exe " (identOrStr)? optConfig : command
 
-@[command_elab leanExeCommand]
+@[builtin_command_elab leanExeCommand]
 def elabLeanExeCommand : CommandElab := fun stx => do
   let `(leanExeCommand|$(doc?)? $(attrs?)? lean_exe%$kw $(nameStx?)? $cfg) := stx
     | throwErrorAt stx "ill-formed lean_exe declaration"
@@ -287,7 +287,7 @@ Can optionally be provided with a configuration of type `InputFileConfig`.
 scoped syntax (name := inputFileCommand)
 (docComment)? (Term.attributes)? "input_file " (identOrStr)? optConfig : command
 
-@[command_elab inputFileCommand]
+@[builtin_command_elab inputFileCommand]
 def elabInputfileCommand : CommandElab := fun stx => do
   let `(inputFileCommand|$(doc?)? $(attrs?)? input_file%$kw $(nameStx?)? $cfg) := stx
     | throwErrorAt stx "ill-formed input_file declaration"
@@ -307,7 +307,7 @@ Can optionally be provided with a configuration of type `InputDirConfig`.
 scoped syntax (name := inputDirCommand)
 (docComment)? (Term.attributes)? "input_dir " (identOrStr)? optConfig : command
 
-@[command_elab inputDirCommand]
+@[builtin_command_elab inputDirCommand]
 def elabInputDirCommand : CommandElab := fun stx => do
   let `(inputDirCommand|$(doc?)? $(attrs?)? input_dir%$kw $(nameStx?)? $cfg) := stx
     | throwErrorAt stx "ill-formed input_dir declaration"
@@ -351,7 +351,7 @@ The term should build the external library's **static** library.
 scoped syntax (name := externLibCommand)
 (docComment)? (Term.attributes)? "extern_lib " externLibDeclSpec : command
 
-@[macro externLibCommand]
+@[builtin_macro externLibCommand]
 def expandExternLibCommand : Macro := fun stx => do
   let `(externLibCommand|$(doc?)? $(attrs?)? extern_lib%$kw $spec) := stx
     | Macro.throwErrorAt stx "ill-formed external library declaration"

src/lake/Lake/DSL/VerLit.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+prelude
+import Lean.Elab.Eval
+import Lake.Util.Version
+
+open Lean Elab Term Meta
+
+/-! # Version Literals
+
+Defines the `v!"<ver>"` syntax for version literals.
+The elaborator attempts to synthesize an instance of `DecodeVersion` for the
+expected type and then applies it to the string literal.
+-/
+
+namespace Lake
+
+instance : ToExpr SemVerCore where
+  toExpr ver := mkAppN (mkConst ``SemVerCore.mk)
+    #[toExpr ver.major, toExpr ver.minor, toExpr ver.patch]
+  toTypeExpr := mkConst ``SemVerCore
+
+instance : ToExpr StdVer where
+  toExpr ver := mkAppN (mkConst ``StdVer.mk)
+    #[toExpr ver.toSemVerCore, toExpr ver.specialDescr]
+  toTypeExpr := mkConst ``StdVer
+
+private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr :=
+  Functor.map toExpr x
+
+/-- A Lake version literal. -/
+scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term
+
+@[builtin_term_elab verLit]
+def elabVerLit : TermElab := fun stx expectedType? => do
+  let `(v!$v) := stx | throwUnsupportedSyntax
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType := expectedType?
+    | throwError "expected type is not known"
+  let ofVerT? ← mkAppM ``Except #[mkConst ``String, expectedType]
+  let ofVerE ← elabTermEnsuringType (← ``(decodeVersion s!$v)) ofVerT?
+  let resT ← mkAppM ``Except #[mkConst ``String, mkConst ``Expr]
+  let resE ← mkAppM ``toResultExpr #[ofVerE]
+  match (← unsafe evalExpr (Except String Expr) resT resE) with
+  | .ok ver => return ver
+  | .error e => throwError e

src/lake/Lake/Load/Lean/Elab.lean

@@ -24,7 +24,7 @@ namespace Lake
 deriving instance BEq, Hashable for Import
 
 /- Cache for the imported header environment of Lake configuration files. -/
-initialize importEnvCache : IO.Ref (Std.HashMap (Array Import) Environment) ← IO.mkRef {}
+builtin_initialize importEnvCache : IO.Ref (Std.HashMap (Array Import) Environment) ← IO.mkRef {}
 
 /-- Like `importModules`, but fetch the resulting import state from the cache if possible. -/
 def importModulesUsingCache (imports : Array Import) (opts : Options) (trustLevel : UInt32) : IO Environment := do

src/lake/Lake/Util/Version.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lean.Elab.Eval
+import Lean.Data.Json
 import Lake.Util.Date
 
 /-! # Version
@@ -53,11 +53,6 @@ instance : ToString SemVerCore := ⟨SemVerCore.toString⟩
 instance : ToJson SemVerCore := ⟨(·.toString)⟩
 instance : FromJson SemVerCore := ⟨(do SemVerCore.parse <| ← fromJson? ·)⟩
 
-instance : ToExpr SemVerCore where
-  toExpr ver := mkAppN (mkConst ``SemVerCore.mk)
-    #[toExpr ver.major, toExpr ver.minor, toExpr ver.patch]
-  toTypeExpr := mkConst ``SemVerCore
-
 /--
 A Lean-style semantic version.
 A major-minor-patch triple with an optional arbitrary `-` suffix.
@@ -114,11 +109,6 @@ instance : ToString StdVer := ⟨StdVer.toString⟩
 instance : ToJson StdVer := ⟨(·.toString)⟩
 instance : FromJson StdVer := ⟨(do StdVer.parse <| ← fromJson? ·)⟩
 
-instance : ToExpr StdVer where
-  toExpr ver := mkAppN (mkConst ``StdVer.mk)
-    #[toExpr ver.toSemVerCore, toExpr ver.specialDescr]
-  toTypeExpr := mkConst ``StdVer
-
 /-- A Lean toolchain version. -/
 inductive ToolchainVer
 | release (ver : LeanVer)
@@ -225,15 +215,6 @@ instance ToolchainVer.decLe (a b : ToolchainVer) : Decidable (a ≤ b) :=
   | .other _, .release _ | .other _, .nightly _ | .other _, .pr _ =>
     .isFalse (by simp [LE.le, ToolchainVer.le])
 
-/-! ## Version Literals
-
-Defines the `v!"<ver>"` syntax for version literals.
-The elaborator attempts to synthesize an instance of `ToVersion` for the
-expected type and then applies it to the string literal.
--/
-
-open Elab Term Meta
-
 /-- Parses a version from a string. -/
 class DecodeVersion (α : Type u) where
   decodeVersion : String → Except String α
@@ -243,23 +224,3 @@ export DecodeVersion (decodeVersion)
 instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩
 @[default_instance] instance : DecodeVersion StdVer := ⟨StdVer.parse⟩
 instance : DecodeVersion ToolchainVer := ⟨(pure <| ToolchainVer.ofString ·)⟩
-
-private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr :=
-  Functor.map toExpr x
-
-/-- A Lake version literal. -/
-scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term
-
-@[term_elab verLit]
-def elabVerLit : TermElab := fun stx expectedType? => do
-  let `(v!$v) := stx | throwUnsupportedSyntax
-  tryPostponeIfNoneOrMVar expectedType?
-  let some expectedType := expectedType?
-    | throwError "expected type is not known"
-  let ofVerT? ← mkAppM ``Except #[mkConst ``String, expectedType]
-  let ofVerE ← elabTermEnsuringType (← ``(decodeVersion s!$v)) ofVerT?
-  let resT ← mkAppM ``Except #[mkConst ``String, mkConst ``Expr]
-  let resE ← mkAppM ``toResultExpr #[ofVerE]
-  match (← unsafe evalExpr (Except String Expr) resT resE) with
-  | .ok ver => return ver
-  | .error e => throwError e

src/lake/tests/setupFile/test.sh

@@ -1,7 +1,10 @@
 #!/usr/bin/env bash
-set -euo pipefail
+set -euxo pipefail
+
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
+./clean.sh
+
 #---
 # Test `setup-file` functionality
 #---
@@ -14,3 +17,8 @@ $LAKE setup-file bogus Foo | grep -F --color '"loadDynlibPaths":[]'
 
 # Test that `setup-file` on an invalid Lean configuration file succeeds.
 $LAKE -f invalid.lean setup-file invalid.lean Lake
+
+# Test that `setup-file` on a configuration file uses the Lake plugin,
+# even if the file is invalid and/or is not using a `Lake` import.
+$LAKE -f invalid.lean setup-file invalid.lean |
+  (grep -F --color '"pluginPaths":[]' && exit 1 || true)