error while building Lean 4

Stream: lean4

[Scott Morrison]

I haven't previously had trouble building Lean 4, but today I am getting the message

CMake Error at shell/CMakeLists.txt:180 (add_test):
  add_test given test NAME "leanlaketest_deps" which already exists in this
  directory.

(and then a bunch of similar ones). Any advice?

[Alex J. Best]

Did you update the lake git submodule? IIRC it got upgraded recently

[Scott Morrison]

The lake submodule already seems to have been updated, and trying again has no effect. Still stuck on this. Here's the complete output.

[Sebastian Ullrich]

To be honest I don't even understand how the corresponding code works (when it does): https://github.com/leanprover/lean4/blob/42a080fae2ef6da9819e1dd998209b237c1042ed/src/shell/CMakeLists.txt#L173-L174
There is no glob, how does it produce more than one result?? I guess it does match the docs... this is pretty cursed even for CMake

The GLOB_RECURSE mode will traverse all the subdirectories of the matched directory and match the files.

[Sebastian Ullrich]

@Scott Morrison Could you add something like

message(STATUS "LEANLAKETESTS: ${LEANLAKETESTS}")

after that line and rerun?

[Scott Morrison]

-- git commit sha1: 256879fdea6e185804c9232e29c5f85e0f32ad20
-- LEANLAKETESTS: /Users/scott/projects/lean/lean4/src/lake/examples/bootstrap/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/deps/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/ffi/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/bootstrap/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/deps/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/ffi/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/git/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/hello/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/init/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/precompile/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/scripts/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/examples/targets/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/102/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/104/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/44/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/49/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/50/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/62/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/75/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/manifest/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lake-packages/hello/test/meta/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/bootstrap/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/deps/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/ffi/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/git/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/hello/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/init/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/precompile/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/scripts/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/examples/targets/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/102/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/104/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/44/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/49/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/50/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/62/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/75/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/manifest/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/lean_packages/hello/test/meta/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/git/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/hello/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/init/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/precompile/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/scripts/test.sh;/Users/scott/projects/lean/lean4/src/lake/examples/targets/test.sh
CMake Error at shell/CMakeLists.txt:181 (add_test):
  add_test given test NAME "leanlaketest_deps" which already exists in this
  directory.

[Sebastian Ullrich]

Ahh, a consequence of the Lake changes https://github.com/leanprover/lean4/commit/c112ae7c580832e3aa951ba2a40bb72fc19cae52. Please remove any untracked files in the lake submodule and try again.

[Scott Morrison]

Eventually worked. git clean -xfd in src/lake/ was apparently insufficient, but deleting src/lake/ then restoring it did the trick.