diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean index 52bdaee071..afdb0a19d9 100644 --- a/src/lake/Lake/Load/Config.lean +++ b/src/lake/Lake/Load/Config.lean @@ -78,3 +78,7 @@ namespace LoadConfig /-- The package's Lake directory (for Lake temporary files). -/ @[inline] public def lakeDir (cfg : LoadConfig) : FilePath := cfg.pkgDir / defaultLakeDir + +/-- The absolute path where compiled configurations are stored. -/ +@[inline] public def configDir (cfg : LoadConfig) : FilePath := + cfg.wsDir / defaultLakeDir / "config" / toString cfg.pkgIdx diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean index c72b295cb0..b3908d0ceb 100644 --- a/src/lake/Lake/Load/Lean/Elab.lean +++ b/src/lake/Lake/Load/Lean/Elab.lean @@ -180,8 +180,7 @@ toolchain). Otherwise, elaborate the configuration and save it to the `.olean`. public def importConfigFile (cfg : LoadConfig) : LogIO Environment := do let some configName := FilePath.mk <$> cfg.configFile.fileName | error "invalid configuration file name" - let pkgName := cfg.pkgName.toString (escape := false) - let configDir := cfg.lakeDir / "config" / pkgName + let configDir := cfg.configDir IO.FS.createDirAll configDir let olean := configDir / configName.withExtension "olean" let traceFile := configDir / configName.withExtension "olean.trace" diff --git a/tests/lake/examples/deps/test.sh b/tests/lake/examples/deps/test.sh index d597b3a197..d526c2852d 100755 --- a/tests/lake/examples/deps/test.sh +++ b/tests/lake/examples/deps/test.sh @@ -16,6 +16,19 @@ $LAKE -d foo build --update ./foo/.lake/build/bin/foo ./bar/.lake/build/bin/bar +# Test compiled configurations are hoisted +test -d foo/.lake/config/0 +test -d foo/.lake/config/1 +test -d foo/.lake/config/2 +test -d foo/.lake/config/3 +test ! -d foo/.lake/config/4 +test -d bar/.lake/config/0 +test -d bar/.lake/config/1 +test -d bar/.lake/config/2 +test -d bar/.lake/config/3 +test -d bar/.lake/config/4 +test ! -d bar/.lake/config/5 + # Test setup-file works (i.e., does not error) $LAKE -d foo setup-file ./foo/Foo.lean @@ -39,3 +52,17 @@ $LAKE -d foo -f lakefile.toml build --update ./foo/.lake/build/bin/foo ./bar/.lake/build/bin/bar + +# Test compiled configurations are hoisted +# and that the TOML configuration produces none +test ! -d foo/.lake/config/0 +test -d foo/.lake/config/1 +test -d foo/.lake/config/2 +test -d foo/.lake/config/3 +test ! -d foo/.lake/config/4 +test ! -d bar/.lake/config/0 +test -d bar/.lake/config/1 +test -d bar/.lake/config/2 +test -d bar/.lake/config/3 +test -d bar/.lake/config/4 +test ! -d bar/.lake/config/5