chore: update tests to account for .lake

2026-03-17 18:34:06 +00:00 · 2023-10-25 02:22:23 -04:00
parent 2ff4821026
commit 4ec3d78afa
87 changed files with 164 additions and 228 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,8 @@
 \#*
 .#*
 *.lock
+.lake
+lake-manifest.json
 build
 !/src/lake/Lake/Build
 GPATH
--- a/src/lake/.gitignore
+++ b/src/lake/.gitignore
@@ -1,4 +1,3 @@
-/build
-/lakefile.olean
-produced.out
-result*
+.lake
+lake-manifest.json
+*produced.out
--- a/src/lake/Makefile
+++ b/src/lake/Makefile
@@ -1,4 +1,4 @@
-LAKE ?= ./build/bin/lake
+LAKE ?= ./.lake/build/bin/lake

 #-------------------------------------------------------------------------------
 # Suite Targets
--- a/src/lake/build.sh
+++ b/src/lake/build.sh
@@ -8,5 +8,5 @@ fi

 LEAN_SYSROOT=${LEAN_SYSROOT:-`lean --print-prefix`}
 LEAN_MAKEFILE="$LEAN_SYSROOT/share/lean/lean.mk"
-EXTRA_ARGS="PKG=Lake OLEAN_OUT=build/lib TEMP_OUT=build/ir BIN_NAME=lake LEAN_PATH=./build/lib LINK_OPTS=$LINK_OPTS"
+EXTRA_ARGS="PKG=Lake OLEAN_OUT=.lake/build/lib TEMP_OUT=.lake/build/ir BIN_NAME=lake LEAN_PATH=./.lake/build/lib LINK_OPTS=$LINK_OPTS"
 PATH="$LEAN_SYSROOT/bin:$PATH" ${MAKE:-make} -f "$LEAN_MAKEFILE" $EXTRA_ARGS bin "$@"
--- a/src/lake/clean-build.sh
+++ b/src/lake/clean-build.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean
+rm -rf .lake
--- a/src/lake/examples/bootstrap/.gitignore
+++ b/src/lake/examples/bootstrap/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/bootstrap/check.sh
+++ b/src/lake/examples/bootstrap/check.sh
@@ -1,4 +1,4 @@
 set -ex

-${LAKE:-./build/bin/lake} --version
-${LAKE:-./build/bin/lake} self-check
+${LAKE:-./.lake/build/bin/lake} --version
+${LAKE:-./.lake/build/bin/lake} self-check
--- a/src/lake/examples/bootstrap/clean.sh
+++ b/src/lake/examples/bootstrap/clean.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/examples/bootstrap/package.sh
+++ b/src/lake/examples/bootstrap/package.sh
@@ -1 +1 @@
-${LAKE:-../../build/bin/lake} build
+${LAKE:-../../.lake/build/bin/lake} build
--- a/src/lake/examples/deps/a/.gitignore
+++ b/src/lake/examples/deps/a/.gitignore
@@ -1,2 +0,0 @@
-/build
-/lakefile.olean
--- a/src/lake/examples/deps/b/.gitignore
+++ b/src/lake/examples/deps/b/.gitignore
@@ -1,2 +0,0 @@
-/build
-/lakefile.olean
--- a/src/lake/examples/deps/bar/.gitignore
+++ b/src/lake/examples/deps/bar/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/deps/clean.sh
+++ b/src/lake/examples/deps/clean.sh
@@ -1,5 +1,2 @@
-rm -rf a/build a/lakefile.olean
-rm -rf b/build b/lakefile.olean
-rm -rf foo/build foo/lakefile.olean foo/lake-manifest.json
-rm -rf bar/build bar/lakefile.olean bar/lake-manifest.json
-rm -rf root/build root/lakefile.olean
+rm -rf root/.lake a/.lake b/.lake foo/.lake bar/.lake
+rm -f foo/lake-manifest.json bar/lake-manifest.json
--- a/src/lake/examples/deps/foo/.gitignore
+++ b/src/lake/examples/deps/foo/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/deps/root/.gitignore
+++ b/src/lake/examples/deps/root/.gitignore
@@ -1,2 +0,0 @@
-/build
-/lakefile.olean
--- a/src/lake/examples/deps/test.sh
+++ b/src/lake/examples/deps/test.sh
@@ -1,27 +1,27 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

 $LAKE -d bar build --update
 $LAKE -d foo build --update

-./foo/build/bin/foo
-./bar/build/bin/bar
+./foo/.lake/build/bin/foo
+./bar/.lake/build/bin/bar

 # Test print-paths works (i.e., does not error)
 $LAKE -d foo print-paths A B

 # Test `lake clean`
-test -d a/build
-test -d b/build
+test -d a/.lake/build
+test -d b/.lake/build
 $LAKE -d foo clean a b
-test ! -d a/build
-test ! -d b/build
-test -d root/build
-test -d foo/build
+test ! -d a/.lake/build
+test ! -d b/.lake/build
+test -d root/.lake/build
+test -d foo/.lake/build
 $LAKE -d foo clean
-test ! -d root/build
-test ! -d foo/build
+test ! -d root/.lake/build
+test ! -d foo/.lake/build
--- a/src/lake/examples/ffi/app/.gitignore
+++ b/src/lake/examples/ffi/app/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/ffi/clean.sh
+++ b/src/lake/examples/ffi/clean.sh
@@ -1,2 +1,2 @@
-rm -rf lib/build lib/lakefile.olean lib/lake-manifest.json
-rm -rf app/build app/lakefile.olean app/lake-manifest.json
+rm -rf lib/.lake lib/lake-manifest.json
+rm -rf app/.lake app/lake-manifest.json
--- a/src/lake/examples/ffi/lib/.gitignore
+++ b/src/lake/examples/ffi/lib/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/ffi/package.sh
+++ b/src/lake/examples/ffi/package.sh
@@ -1,10 +1,10 @@
 set -ex

 cd app
-${LAKE:-../../../build/bin/lake} build -v -U
+${LAKE:-../../../.lake/build/bin/lake} build -v -U
 cd ..


 cd lib
-${LAKE:-../../../build/bin/lake} build -v
+${LAKE:-../../../.lake/build/bin/lake} build -v
 cd ..
--- a/src/lake/examples/ffi/test.sh
+++ b/src/lake/examples/ffi/test.sh
@@ -2,7 +2,7 @@ set -ex

 ./clean.sh
 ./package.sh
-./app/build/bin/app
-./lib/build/bin/test
+./app/.lake/build/bin/app
+./lib/.lake/build/bin/test

-${LAKE:-../../build/bin/lake} -d app build -v Test
+${LAKE:-../../.lake/build/bin/lake} -d app build -v Test
--- a/src/lake/examples/hello/.gitignore
+++ b/src/lake/examples/hello/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/hello/bootstrapped-test.sh
+++ b/src/lake/examples/hello/bootstrapped-test.sh
@@ -1,3 +1,3 @@
 ./clean.sh
-${LAKE:-../bootstrap/build/bin/lake} build
-./build/bin/hello
+${LAKE:-../bootstrap/.lake/build/bin/lake} build
+./.lake/build/bin/hello
--- a/src/lake/examples/hello/clean.sh
+++ b/src/lake/examples/hello/clean.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/examples/hello/package.sh
+++ b/src/lake/examples/hello/package.sh
@@ -1 +1 @@
-${LAKE:-../../build/bin/lake} build
+${LAKE:-../../.lake/build/bin/lake} build
--- a/src/lake/examples/hello/test.sh
+++ b/src/lake/examples/hello/test.sh
@@ -1,12 +1,12 @@
 set -ex

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

 $LAKE exe hello
 $LAKE exe hello Bob Bill
-build/bin/hello
+.lake/build/bin/hello

 # Tests that build produces a manifest if there is none.
 # Related: https://github.com/leanprover/lean4/issues/2549
--- a/src/lake/examples/precompile/bar/.gitignore
+++ b/src/lake/examples/precompile/bar/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/precompile/clean.sh
+++ b/src/lake/examples/precompile/clean.sh
@@ -1,2 +1,2 @@
-rm -rf foo/build foo/lakefile.olean foo/lake-manifest.json
-rm -rf bar/build bar/lakefile.olean bar/lake-manifest.json
+rm -rf foo/.lake foo/lake-manifest.json
+rm -rf bar/.lake bar/lake-manifest.json
--- a/src/lake/examples/precompile/foo/.gitignore
+++ b/src/lake/examples/precompile/foo/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/precompile/test.sh
+++ b/src/lake/examples/precompile/test.sh
@@ -1,6 +1,6 @@
 set -ex

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh
 $LAKE -d bar update
--- a/src/lake/examples/reverse-ffi/Makefile
+++ b/src/lake/examples/reverse-ffi/Makefile
@@ -16,17 +16,17 @@ $(OUT_DIR):

 ifneq ($(OS),Windows_NT)
 # Add shared library paths to loader path (no Windows equivalent)
-LINK_FLAGS=-Wl,-rpath,$(LEAN_LIBDIR) -Wl,-rpath,$(PWD)/lib/build/lib
+LINK_FLAGS=-Wl,-rpath,$(LEAN_LIBDIR) -Wl,-rpath,$(PWD)/lib/.lake/build/lib
 endif

 $(OUT_DIR)/main: main.c lake | $(OUT_DIR)
 # Add library paths for Lake package and for Lean itself
-	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/build/lib -lRFFI -lleanshared $(LINK_FLAGS)
+	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lleanshared $(LINK_FLAGS)

 run: $(OUT_DIR)/main
 ifeq ($(OS),Windows_NT)
 # Add shared library paths to loader path dynamically
-	env PATH="lib/build/lib:$(shell cygpath $(LEAN_SYSROOT))/bin:$(PATH)" $(OUT_DIR)/main
+	env PATH="lib/.lake/build/lib:$(shell cygpath $(LEAN_SYSROOT))/bin:$(PATH)" $(OUT_DIR)/main
 else
 	$(OUT_DIR)/main
 endif
@@ -52,7 +52,7 @@ LEAN_SHLIB=$(LEAN_LIBDIR)/libleanshared.$(SHLIB_EXT)
 endif

 $(OUT_DIR)/main-local: main.c lake | $(OUT_DIR)
-	cp -f $(LEAN_SHLIB) lib/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
+	cp -f $(LEAN_SHLIB) lib/.lake/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
 	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lleanshared $(LINK_FLAGS_LOCAL)

 run-local: $(OUT_DIR)/main-local
--- a/src/lake/examples/reverse-ffi/clean.sh
+++ b/src/lake/examples/reverse-ffi/clean.sh
@@ -1 +1 @@
-rm -rf out lib/build lib/lakefile.olean lib/lake-manifest.json
+rm -rf out lib/.lake lib/lake-manifest.json
--- a/src/lake/examples/reverse-ffi/lib/.gitignore
+++ b/src/lake/examples/reverse-ffi/lib/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/scripts/.gitignore
+++ b/src/lake/examples/scripts/.gitignore
@@ -1,2 +0,0 @@
-lakefile.olean
-lake-manifest.json
--- a/src/lake/examples/scripts/clean.sh
+++ b/src/lake/examples/scripts/clean.sh
@@ -1 +1 @@
-rm -f lakefile.olean lake-manifest.json produced.out
+rm -rf .lake dep/.lake lake-manifest.json produced.out
--- a/src/lake/examples/scripts/test.sh
+++ b/src/lake/examples/scripts/test.sh
@@ -5,7 +5,7 @@ set -exo pipefail
 [ "$OSTYPE" == "msys" ] && export MSYS2_ARG_CONV_EXCL=*

 ./clean.sh
-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 $LAKE update
 $LAKE script list | tee produced.out
--- a/src/lake/examples/targets/.gitignore
+++ b/src/lake/examples/targets/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-manifest.json
--- a/src/lake/examples/targets/clean.sh
+++ b/src/lake/examples/targets/clean.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/examples/targets/test.sh
+++ b/src/lake/examples/targets/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 if [ "$OS" = Windows_NT ]; then
 LIB_PREFIX=
@@ -28,53 +28,53 @@ $LAKE build foo:print_name | grep -m1 foo

 # Test the module `deps` facet
 $LAKE build Foo:deps
-test -f ./build/lib/Foo/Bar.olean
-test ! -f ./build/lib/Foo.olean
+test -f ./.lake/build/lib/Foo/Bar.olean
+test ! -f ./.lake/build/lib/Foo.olean

 # Test the module specifier
-test ! -f ./build/lib/Foo/Baz.olean
+test ! -f ./.lake/build/lib/Foo/Baz.olean
 $LAKE build +Foo.Baz
-test -f ./build/lib/Foo/Baz.olean
+test -f ./.lake/build/lib/Foo/Baz.olean

 # Test `.c.o` specifier
-test ! -f ./build/ir/Bar.c.o
+test ! -f ./.lake/build/ir/Bar.c.o
 $LAKE build Bar:o
-test -f ./build/ir/Bar.c.o
+test -f ./.lake/build/ir/Bar.c.o

 # Test default targets
-test ! -f ./build/bin/c
-test ! -f ./build/lib/Foo.olean
-test ! -f ./build/lib/${LIB_PREFIX}Foo.a
-test ! -f ./build/meow.txt
+test ! -f ./.lake/build/bin/c
+test ! -f ./.lake/build/lib/Foo.olean
+test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo.a
+test ! -f ./.lake/build/meow.txt
 $LAKE build targets/
-./build/bin/c
-test -f ./build/lib/Foo.olean
-test -f ./build/lib/${LIB_PREFIX}Foo.a
-cat ./build/meow.txt | grep -m1 Meow!
+./.lake/build/bin/c
+test -f ./.lake/build/lib/Foo.olean
+test -f ./.lake/build/lib/${LIB_PREFIX}Foo.a
+cat ./.lake/build/meow.txt | grep -m1 Meow!

 # Test shared lib facets
-test ! -f ./build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT
-test ! -f ./build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT
+test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT
+test ! -f ./.lake/build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT
 $LAKE build foo:shared bar
-test -f ./build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT
-test -f ./build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT
+test -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT
+test -f ./.lake/build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT

 # Test dynlib facet
-test ! -f ./build/lib/${LIB_PREFIX}Foo-1.$SHARED_LIB_EXT
+test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo-1.$SHARED_LIB_EXT
 $LAKE build Foo:dynlib
-test -f ./build/lib/${LIB_PREFIX}Foo-1.$SHARED_LIB_EXT
+test -f ./.lake/build/lib/${LIB_PREFIX}Foo-1.$SHARED_LIB_EXT

 # Test library `extraDepTargets`
-test ! -f ./build/caw.txt
-test ! -f ./build/lib/Baz.olean
+test ! -f ./.lake/build/caw.txt
+test ! -f ./.lake/build/lib/Baz.olean
 $LAKE build baz
-test -f ./build/lib/Baz.olean
-cat ./build/caw.txt | grep -m1 Caw!
+test -f ./.lake/build/lib/Baz.olean
+cat ./.lake/build/caw.txt | grep -m1 Caw!

 # Test executable build
 $LAKE build a b
-./build/bin/a
-./build/bin/b
+./.lake/build/bin/a
+./.lake/build/bin/b

 # Test repeat build works
 $LAKE build bark | grep -m1 Bark!
--- a/src/lake/tests/.gitignore
+++ b/src/lake/tests/.gitignore
@@ -1,5 +0,0 @@
-build
-lake-packages
-lakefile.olean
-lake-manifest.json
-*produced.out
--- a/src/lake/tests/badImport/clean.sh
+++ b/src/lake/tests/badImport/clean.sh
@@ -1 +1 @@
-rm -rf build lake-manifest.json lakefile.olean
+rm -rf .lake lake-manifest.json
--- a/src/lake/tests/badImport/test.sh
+++ b/src/lake/tests/badImport/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

--- a/src/lake/tests/buildArgs/clean.sh
+++ b/src/lake/tests/buildArgs/clean.sh
@@ -1 +1 @@
-rm -rf build lake-manifest.json lakefile.olean produced.out
+rm -rf .lake lake-manifest.json produced.out
--- a/src/lake/tests/buildArgs/test.sh
+++ b/src/lake/tests/buildArgs/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 if [ "`uname`" = Darwin ]; then
  sed_i() { sed -i '' "$@"; }
@@ -36,15 +36,15 @@ ${LAKE} build +Hello:o -R -KweakLeancArgs=-DBAR | tee -a produced.out
 ${LAKE} build +Hello:dynlib Hello:shared hello -R
 echo "# link args" >> produced.out
 # Use `head -n1` to avoid extraneous warnings on MacOS with current Lean (6/8/23)
-${LAKE} build +Hello:dynlib -R -KlinkArgs=-Lbuild/lib | head -n1 | tee -a produced.out
-${LAKE} build Hello:shared -R -KlinkArgs=-Lbuild/lib | head -n1 | tee -a produced.out
-${LAKE} build hello -R -KlinkArgs=-Lbuild/lib | head -n1 | tee -a produced.out
+${LAKE} build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib | head -n1 | tee -a produced.out
+${LAKE} build Hello:shared -R -KlinkArgs=-L.lake/build/lib | head -n1 | tee -a produced.out
+${LAKE} build hello -R -KlinkArgs=-L.lake/build/lib | head -n1 | tee -a produced.out

 ${LAKE} build +Hello:dynlib Hello:shared hello  -R
 echo "# weak link args" >> produced.out
-${LAKE} build +Hello:dynlib -R -KweakLinkArgs=-Lbuild/lib | tee -a produced.out
-${LAKE} build Hello:shared -R -KweakLinkArgs=-Lbuild/lib | tee -a produced.out
-${LAKE} build hello -R -KweakLinkArgs=-Lbuild/lib | tee -a produced.out
+${LAKE} build +Hello:dynlib -R -KweakLinkArgs=-L.lake/build/lib | tee -a produced.out
+${LAKE} build Hello:shared -R -KweakLinkArgs=-L.lake/build/lib | tee -a produced.out
+${LAKE} build hello -R -KweakLinkArgs=-L.lake/build/lib | tee -a produced.out

 # check output against the expected output
 sed_i 's/lib//g' produced.out # remove lib prefixes
--- a/src/lake/tests/clone/clean.sh
+++ b/src/lake/tests/clone/clean.sh
@@ -1,4 +1,2 @@
 rm -rf hello
-rm -rf test/build test/lakefile.olean
-rm -rf test/lake-packages
-rm -f test/lake-manifest.json
+rm -rf test/.lake test/lake-manifest.json
--- a/src/lake/tests/clone/test.sh
+++ b/src/lake/tests/clone/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../../build/bin/lake}
+LAKE=${LAKE:-../../../.lake/build/bin/lake}

 if [ "`uname`" = Darwin ]; then
  sed_i() { sed -i '' "$@"; }
@@ -32,7 +32,7 @@ LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update | grep "file://"
 # test that a second `lake update` is a no-op (with URLs)
 # see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901
 LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update | diff - /dev/null
-rm -rf lake-packages
+rm -rf .lake/packages

 # Test that Lake produces no warnings on a `lake build` after a `lake update`
 # See https://github.com/leanprover/lean4/issues/2427
@@ -40,19 +40,19 @@ rm -rf lake-packages
 $LAKE update
 # test that a second `lake update` is a no-op (with file paths)
 $LAKE update | diff - /dev/null
-test -d lake-packages/hello
+test -d .lake/packages/hello
 # test that Lake produces no warnings
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
-./build/bin/test | grep "Hello, world"
+./.lake/build/bin/test | grep "Hello, world"

 # Test that Lake produces a warning if local changes are made to a dependency
 # See https://github.com/leanprover/lake/issues/167

-sed_i "s/world/changes/" lake-packages/hello/Hello/Basic.lean
-! git -C lake-packages/hello diff --exit-code
+sed_i "s/world/changes/" .lake/packages/hello/Hello/Basic.lean
+! git -C .lake/packages/hello diff --exit-code
 $LAKE build 3>&1 1>&2 2>&3 | grep "has local changes"
-./build/bin/test | grep "Hello, changes"
-git -C lake-packages/hello reset --hard
+./.lake/build/bin/test | grep "Hello, changes"
+git -C .lake/packages/hello reset --hard
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null

 # Test no `git fetch` on a `lake build` if already on the proper revision
@@ -62,7 +62,7 @@ TEST_URL=https://example.com/hello.git
 TEST_MAP="{\"hello\" : \"$TEST_URL\"}"

 # set invalid remote
-git -C lake-packages/hello remote set-url origin $TEST_URL
+git -C .lake/packages/hello remote set-url origin $TEST_URL
 # build should succeed (do nothing) despite the invalid remote because
 # the remote should not be fetched; Lake should also not produce any warnings
 LAKE_PKG_URL_MAP=$TEST_MAP $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
--- a/src/lake/tests/clone/test/.gitignore
+++ b/src/lake/tests/clone/test/.gitignore
@@ -1,4 +0,0 @@
-/build
-/lakefile.olean
-/lake-packages
-lake-manifest.json
--- a/src/lake/tests/depTree/test.sh
+++ b/src/lake/tests/depTree/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-$PWD/../../build/bin/lake}
+LAKE=${LAKE:-$PWD/../../.lake/build/bin/lake}

 if [ "`uname`" = Darwin ]; then
  sed_i() { sed -i '' "$@"; }
@@ -108,7 +108,7 @@ popd
 pushd d
 $LAKE update -v
 # test 70: we do not update transitive depednecies
-! grep 'third commit in a' lake-packages/a/A.lean
+! grep 'third commit in a' .lake/packages/a/A.lean
 git diff --exit-code
 popd

@@ -132,7 +132,7 @@ pushd d
 # d: b@1 -> b@2 => a@1 -> a@3
 $LAKE update b -v
 # test 119: pickup a@3 and not a@4
-grep 'third commit in a' lake-packages/a/A.lean
+grep 'third commit in a' .lake/packages/a/A.lean
 # test the removal of `c` from the manifest
 grep "\"c\"" lake-manifest.json
 sed_i '/require c/d' lakefile.lean
--- a/src/lake/tests/env/test.sh
+++ b/src/lake/tests/env/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 # Test the functionality of `lake env`
 # Also test https://github.com/leanprover/lake/issues/179
--- a/src/lake/tests/globs/.gitignore
+++ b/src/lake/tests/globs/.gitignore
@@ -1,2 +0,0 @@
-/build
-/lakefile.olean
--- a/src/lake/tests/globs/clean.sh
+++ b/src/lake/tests/globs/clean.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/tests/globs/test.sh
+++ b/src/lake/tests/globs/test.sh
@@ -3,15 +3,15 @@ set -euxo pipefail

 ./clean.sh

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 # test that directory information is preserved during glob recursion
 # see https://github.com/leanprover/lake/issues/102

 $LAKE build TBA
-test -f build/lib/TBA.olean
-test -f build/lib/TBA/Eulerian.olean
-test -f build/lib/TBA/Eulerian/A.olean
+test -f .lake/build/lib/TBA.olean
+test -f .lake/build/lib/TBA/Eulerian.olean
+test -f .lake/build/lib/TBA/Eulerian/A.olean

 # test that globs capture modules with non-Lean names
 # see https://github.com/leanprover/lake/issues/174
@@ -20,6 +20,6 @@ test -f build/lib/TBA/Eulerian/A.olean
 # see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20build.20all/near/370788618

 $LAKE build Test
-test -f build/lib/Test/1.olean
-test -f build/lib/Test/Subtest/1.olean
+test -f .lake/build/lib/Test/1.olean
+test -f .lake/build/lib/Test/Subtest/1.olean

--- a/src/lake/tests/init/test.sh
+++ b/src/lake/tests/init/test.sh
@@ -2,8 +2,8 @@ set -ex

 ./clean.sh

-LAKE1=${LAKE:-../../../build/bin/lake}
-LAKE=${LAKE:-../../build/bin/lake}
+LAKE1=${LAKE:-../../../.lake/build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 # Test `new` and `init` with bad template (should error)

@@ -15,13 +15,13 @@ LAKE=${LAKE:-../../build/bin/lake}

 $LAKE new Hello
 $LAKE -d Hello build
-Hello/build/bin/hello
+Hello/.lake/build/bin/hello

 # Test creating multi-level packages with a `.`

 $LAKE new hello.world
 $LAKE -d hello-world build
-hello-world/build/bin/hello-world
+hello-world/.lake/build/bin/hello-world
 test -f hello-world/Hello/World/Basic.lean

 # Test creating packages with a `-` (i.e., a non-Lean name)
@@ -29,14 +29,14 @@ test -f hello-world/Hello/World/Basic.lean

 $LAKE new lean-data
 $LAKE -d lean-data build
-lean-data/build/bin/lean-data
+lean-data/.lake/build/bin/lean-data

 # Test creating packages with keyword names
 # https://github.com/leanprover/lake/issues/128

 $LAKE new meta
 $LAKE -d meta build
-meta/build/bin/meta
+meta/.lake/build/bin/meta

 # Test `init`

@@ -45,7 +45,7 @@ mkdir hello_world
 cd hello_world
 $LAKE1 init hello_world exe
 $LAKE1 build
-./build/bin/hello_world
+./.lake/build/bin/hello_world

 # Test `init` on existing package (should error)

--- a/src/lake/tests/llvm-bitcode-gen/.gitignore
+++ b/src/lake/tests/llvm-bitcode-gen/.gitignore
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-packages/*
--- a/src/lake/tests/llvm-bitcode-gen/clean.sh
+++ b/src/lake/tests/llvm-bitcode-gen/clean.sh
@@ -1,3 +1 @@
-rm -rf build
-rm -rf lakefile.olean
-rm -rf lake-manifest.json
+rm -rf .lake
--- a/src/lake/tests/llvm-bitcode-gen/lake-manifest.json
+++ b/src/lake/tests/llvm-bitcode-gen/lake-manifest.json
@@ -1,4 +0,0 @@
-{"version": 6,
- "packagesDir": "lake-packages",
- "packages": [],
- "name": "«llvm-bitcode-gen»"}
--- a/src/lake/tests/llvm-bitcode-gen/test.sh
+++ b/src/lake/tests/llvm-bitcode-gen/test.sh
@@ -20,8 +20,8 @@ lake script run llvm-bitcode-gen/hasLLVMBackend | grep "true"
 # If we have the LLVM backend in the Lean toolchain, then we expect this to
 # print `true`, as this queries the same flag that Lake queries to check the presence
 # of the LLVM toolchian.
-./build/bin/llvm-bitcode-gen | grep 'true'
+./.lake/build/bin/llvm-bitcode-gen | grep 'true'

 # If we have the LLVM backend, check that lake builds bitcode artefacts.
-test -f build/ir/LlvmBitcodeGen.bc
-test -f build/ir/Main.bc
+test -f .lake/build/ir/LlvmBitcodeGen.bc
+test -f .lake/build/ir/Main.bc
--- a/src/lake/tests/lock/clean.sh
+++ b/src/lake/tests/lock/clean.sh
@@ -1,2 +1,2 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
 rm -f test*.log
--- a/src/lake/tests/lock/test.sh
+++ b/src/lake/tests/lock/test.sh
@@ -4,7 +4,7 @@ set -euxo pipefail
 echo "lock file currently disabled; skipping test"
 exit 0

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 if [ "`uname`" = Darwin ]; then
  TAIL=gtail
@@ -19,31 +19,31 @@ touch test1.log
 $LAKE build Loop 1> test1.log &
 test1_pid=$!
 grep -q "Building" < <($TAIL --pid=$$ -f test1.log)
-test -f build/lake.lock
+test -f .lake/build/lake.lock
 kill $test1_pid
 ! wait $test1_pid

 # Test build waits when lock file present
 touch test2.log
-touch build/lake.lock
+touch .lake/build/lake.lock
 $LAKE build Nop 2> test2.log &
 test2_pid=$!
 grep -q "waiting" < <($TAIL --pid=$$ -f test2.log)
 # Test build resumes on lock file removal
-rm build/lake.lock
+rm .lake/build/lake.lock
 wait $test2_pid
 # Test build success does not leave lock file
-test ! -f build/lake.lock
+test ! -f .lake/build/lake.lock

 # Test build error still deletes lock file
 ! $LAKE build Error
-test ! -f build/lake.lock
+test ! -f .lake/build/lake.lock

 # Test that removing the lock during build does not cause it to fail
 touch test3.log
 $LAKE build Wait > test3.log 2>&1 &
 test3_pid=$!
 grep -q "Building" < <($TAIL --pid=$$ -f test3.log)
-rm build/lake.lock
+rm .lake/build/lake.lock
 wait $test3_pid
 cat test3.log | grep "deleted before the lock"
--- a/src/lake/tests/meta/clean.sh
+++ b/src/lake/tests/meta/clean.sh
@@ -1 +1 @@
-rm -f lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/tests/meta/test.sh
+++ b/src/lake/tests/meta/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 $LAKE resolve-deps -R 2>&1
 $LAKE resolve-deps -R 2>&1 | grep "impure"
--- a/src/lake/tests/noBuild/clean.sh
+++ b/src/lake/tests/noBuild/clean.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/tests/noBuild/test.sh
+++ b/src/lake/tests/noBuild/test.sh
@@ -7,18 +7,18 @@ set -euxo pipefail
 ./clean.sh

 NO_BUILD_CODE=3
-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 # Test `--no-build` for print-paths and module builds (`buildUnlessUpToDate`)
 $LAKE print-paths Test --no-build && exit 1 || [ $? = $NO_BUILD_CODE ]
-test ! -f build/lib/Test.olean
+test ! -f .lake/build/lib/Test.olean
 $LAKE build Test
-test -f build/lib/Test.olean
+test -f .lake/build/lib/Test.olean
 $LAKE print-paths Test --no-build

 # Test `--no-build` for file builds (`buildFileUnlessUpToDate`)
 $LAKE build +Test:o --no-build && exit 1 || [ $? = $NO_BUILD_CODE ]
-test ! -f build/ir/Test.c.o
+test ! -f .lake/build/ir/Test.c.o
 $LAKE build +Test:o
-test -f build/ir/Test.c.o
+test -f .lake/build/ir/Test.c.o
 $LAKE build +Test:o --no-build
--- a/src/lake/tests/old/test.sh
+++ b/src/lake/tests/old/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

--- a/src/lake/tests/order/clean.sh
+++ b/src/lake/tests/order/clean.sh
@@ -1,5 +1,3 @@
-rm -rf build foo/build bar/build
-rm -f lakefile.olean foo/lakefile.olean bar/lakefile.olean
+rm -rf .lake foo/.lake bar/.lake
 rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json
-rm -rf lake-packages
 rm -f lake-manifest-1.json
--- a/src/lake/tests/order/test.sh
+++ b/src/lake/tests/order/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

--- a/src/lake/tests/postUpdate/clean.sh
+++ b/src/lake/tests/postUpdate/clean.sh
@@ -1,2 +1,2 @@
-rm -rf dep/build dep/lakefile.olean dep/toolchain dep/lake-manifest.json
-rm -f lake-manifest.json lakefile.olean lake-manifest.json toolchain
+rm -rf dep/.lake dep/toolchain dep/lake-manifest.json
+rm -rf .lake lake-manifest.json toolchain
--- a/src/lake/tests/postUpdate/test.sh
+++ b/src/lake/tests/postUpdate/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

--- a/src/lake/tests/precompileArgs/clean.sh
+++ b/src/lake/tests/precompileArgs/clean.sh
@@ -1 +1 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
--- a/src/lake/tests/precompileArgs/test.sh
+++ b/src/lake/tests/precompileArgs/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -exo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

--- a/src/lake/tests/rebuild/clean.sh
+++ b/src/lake/tests/rebuild/clean.sh
@@ -1,2 +1,2 @@
-rm -rf build lakefile.olean lake-manifest.json
+rm -rf .lake lake-manifest.json
 rm -rf Foo Foo.lean
--- a/src/lake/tests/rebuild/test.sh
+++ b/src/lake/tests/rebuild/test.sh
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 ./clean.sh

@@ -15,9 +15,9 @@ mkdir -p Foo
 echo $'def a := "a"' > Foo/Test.lean
 echo $'import Foo.Test def hello := a' > Foo.lean
 ${LAKE} build
-./build/bin/foo | grep -m1 a
+./.lake/build/bin/foo | grep -m1 a
 echo $'def b := "b"' > Foo/Test.lean
 echo $'import Foo.Test def hello := b' > Foo.lean
 ${LAKE} build Foo
 ${LAKE} build
-./build/bin/foo | grep -m1 b
+./.lake/build/bin/foo | grep -m1 b
--- a/src/lake/tests/serve/clean.sh
+++ b/src/lake/tests/serve/clean.sh
@@ -1 +1 @@
-rm -f lakefile.lean lakefile.olean
+rm -rf .lake lakefile.lean
--- a/src/lake/tests/serve/test.sh
+++ b/src/lake/tests/serve/test.sh
@@ -7,7 +7,7 @@ else
  TAIL=tail
 fi

-LAKE=${LAKE:-../../build/bin/lake}
+LAKE=${LAKE:-../../.lake/build/bin/lake}

 INIT_REQ=$'Content-Length: 46\r\n\r\n{"jsonrpc":"2.0","method":"initialize","id":1}'
 INITD_NOT=$'Content-Length: 40\r\n\r\n{"jsonrpc":"2.0","method":"initialized"}'
@@ -24,7 +24,7 @@ echo "does not compile" > lakefile.lean
 # ---

 MSGS="$INIT_REQ$INITD_NOT$SD_REQ$EXIT_NOT"
-echo -n "$MSGS" | ${LAKE:-../../build/bin/lake} serve >/dev/null
+echo -n "$MSGS" | ${LAKE:-../../.lake/build/bin/lake} serve >/dev/null
 echo "tested 49"

 # ---
--- a/src/lake/tests/toolchain/test.sh
+++ b/src/lake/tests/toolchain/test.sh
@@ -23,4 +23,4 @@ cd foo
 elan run leanprover/lean4:nightly-2022-06-30 lake build +Foo:olean | grep -m1 Foo.olean
 rm lean-toolchain
 sed_i 's/defaultTarget/default_target/g' lakefile.lean
-${LAKE:-../../../build/bin/lake} build -v | grep -m1 Foo.olean
+${LAKE:-../../../.lake/build/bin/lake} build -v | grep -m1 Foo.olean
--- a/src/lake/time-build.sh
+++ b/src/lake/time-build.sh
@@ -1,2 +1,2 @@
-./clean.sh
+./clean-build.sh
 time ./build.sh "$@"
--- a/tests/pkg/builtin_attr/test.sh
+++ b/tests/pkg/builtin_attr/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build
--- a/tests/pkg/deriving/test.sh
+++ b/tests/pkg/deriving/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build
--- a/tests/pkg/frontend/Frontend/Compile.lean
+++ b/tests/pkg/frontend/Frontend/Compile.lean
@@ -15,8 +15,8 @@ unsafe def processInput (input : String) (initializers := false)  :
 open System in
 def findLean (mod : Name) : IO FilePath := do
  let olean ← findOLean mod
-  -- Remove a "build/lib/" substring from the path.
-  let lean := olean.toString.replace (toString (FilePath.mk "build" / "lib") ++ FilePath.pathSeparator.toString) ""
+  -- Remove a ".lake/build/lib/" substring from the path.
+  let lean := olean.toString.replace (toString (FilePath.mk ".lake" / "build" / "lib") ++ FilePath.pathSeparator.toString) ""
  return FilePath.mk lean |>.withExtension "lean"

 /-- Read the source code of the named module. -/
--- a/tests/pkg/frontend/test.sh
+++ b/tests/pkg/frontend/test.sh
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build

 # Check that we can compile a file which shares with the executable
--- a/tests/pkg/misc/test.sh
+++ b/tests/pkg/misc/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build
--- a/tests/pkg/prv/test.sh
+++ b/tests/pkg/prv/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build 2>&1 | grep 'error: field.*private'
--- a/tests/pkg/user_attr/test.sh
+++ b/tests/pkg/user_attr/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build
--- a/tests/pkg/user_attr_app/Main.lean
+++ b/tests/pkg/user_attr_app/Main.lean
@@ -12,5 +12,5 @@ def tst : MetaM Unit := do
 #eval tst

 unsafe def main : IO Unit := do
-  initSearchPath (← Lean.findSysroot) ["build/lib"]
+  initSearchPath (← Lean.findSysroot) [".lake/build/lib"]
  withImportModules #[{ module := `UserAttr.Tst : Import }] {} 0 fun env => pure ()
--- a/tests/pkg/user_attr_app/test.sh
+++ b/tests/pkg/user_attr_app/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
-lake build && ./build/bin/user_attr
+rm -rf .lake/build
+lake build && ./.lake/build/bin/user_attr
--- a/tests/pkg/user_ext/test.sh
+++ b/tests/pkg/user_ext/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build -v 2>&1 | grep 'hello, test, world'
--- a/tests/pkg/user_opt/test.sh
+++ b/tests/pkg/user_opt/test.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash

-rm -rf build
+rm -rf .lake/build
 lake build