diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean
index 1491d7de71..49c2bbab93 100644
--- a/src/lake/Lake/CLI/Serve.lean
+++ b/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
diff --git a/src/lake/Lake/DSL.lean b/src/lake/Lake/DSL.lean
index 36f1d956f0..6b906b6476 100644
--- a/src/lake/Lake/DSL.lean
+++ b/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
diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean
index ad9ef0e3e5..9bcc07a7bf 100644
--- a/src/lake/Lake/DSL/Attributes.lean
+++ b/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
diff --git a/src/lake/Lake/DSL/AttributesCore.lean b/src/lake/Lake/DSL/AttributesCore.lean
index 1b5408da6b..7ce6b40cbb 100644
--- a/src/lake/Lake/DSL/AttributesCore.lean
+++ b/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"
diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean
index 20c9bd8ccb..766415a13f 100644
--- a/src/lake/Lake/DSL/Config.lean
+++ b/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
diff --git a/src/lake/Lake/DSL/Extensions.lean b/src/lake/Lake/DSL/Extensions.lean
index 150805a4f9..b9fe936eba 100644
--- a/src/lake/Lake/DSL/Extensions.lean
+++ b/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)
diff --git a/src/lake/Lake/DSL/Meta.lean b/src/lake/Lake/DSL/Meta.lean
index b9e5a02c92..8b887f0196 100644
--- a/src/lake/Lake/DSL/Meta.lean
+++ b/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
diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean
index 873900e531..d7dff2a7b7 100644
--- a/src/lake/Lake/DSL/Package.lean
+++ b/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]?) =>
diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean
index 8d9b22fd5c..684622d085 100644
--- a/src/lake/Lake/DSL/Require.lean
+++ b/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"
diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean
index 9565f0cf88..05312de6be 100644
--- a/src/lake/Lake/DSL/Script.lean
+++ b/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]?)
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index afab66dc71..985bb43111 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/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"
diff --git a/src/lake/Lake/DSL/VerLit.lean b/src/lake/Lake/DSL/VerLit.lean
new file mode 100644
index 0000000000..292197d511
--- /dev/null
+++ b/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
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index a8339c2b6e..9ba6ca06e9 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/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
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index ac8e1e551a..22eb4048e6 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/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
diff --git a/src/lake/tests/setupFile/test.sh b/src/lake/tests/setupFile/test.sh
index 58c944e701..c201dce4db 100755
--- a/src/lake/tests/setupFile/test.sh
+++ b/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)