From a35c62d0adca26c196774791870e14685e8537dd Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 7 Apr 2025 23:45:33 -0400 Subject: [PATCH] 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 | 1 + src/lake/Lake/DSL.lean | 1 + src/lake/Lake/DSL/Attributes.lean | 2 +- src/lake/Lake/DSL/AttributesCore.lean | 34 +++++++++---------- src/lake/Lake/DSL/Config.lean | 4 +-- src/lake/Lake/DSL/Extensions.lean | 4 +-- src/lake/Lake/DSL/Meta.lean | 4 +-- src/lake/Lake/DSL/Package.lean | 4 +-- src/lake/Lake/DSL/Require.lean | 2 +- src/lake/Lake/DSL/Script.lean | 2 +- src/lake/Lake/DSL/Targets.lean | 18 +++++----- src/lake/Lake/DSL/VerLit.lean | 49 +++++++++++++++++++++++++++ src/lake/Lake/Load/Lean/Elab.lean | 2 +- src/lake/Lake/Util/Version.lean | 41 +--------------------- src/lake/tests/setupFile/test.sh | 10 +++++- 15 files changed, 99 insertions(+), 79 deletions(-) create mode 100644 src/lake/Lake/DSL/VerLit.lean 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!""` 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!""` 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)