Lake test failure

gistfile1.txt

test 2057
    Start 2057: leanlaketest_init

2057: Test command: /bin/bash "-c" "
               set -eu
               export PATH=/Users/leomoura/projects/lean4/build/release/stage1/bin:$PATH LEAN_CC=/usr/bin/clang CXX='/usr/bin/clang++  -O3 -DNDEBUG' LEANC_OPTS=' -O3 -DNDEBUG'
               LAKE=lake ./test.sh"
2057: Working Directory: /Users/leomoura/projects/lean4/src/lake/tests/init
2057: Test timeout computed to be: 1500
2057: + ./clean.sh
2057: ++ uname
2057: + unamestr=Darwin
2057: + '[' Darwin = Darwin ']'
2057: + LAKE1=lake
2057: + LAKE=lake
2057: + lake new foo bar
2057: + grep --color 'unknown package template'
2057: + true
2057: error: unknown package template `bar`
2057: + lake new foo .baz
2057: + grep --color 'unknown configuration language'
2057: + true
2057: error: unknown configuration language `baz`
2057: + lake init foo bar
2057: + grep --color 'unknown package template'
2057: + true
2057: error: unknown package template `bar`
2057: + lake init foo std.baz
2057: + grep --color 'unknown configuration language'
2057: + true
2057: error: unknown configuration language `baz`
2057: + lake new .
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name '.'
2057: + for cmd in new init
2057: + lake new ..
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name '..'
2057: + lake new ....
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name '....'
2057: + lake new '  '
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name ''
2057: + lake new a/bc
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name 'a/bc'
2057: + lake new 'a\b'
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name 'a\b'
2057: + lake new init
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake new Lean
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake new Lake
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake new main
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + for cmd in new init
2057: + lake init ..
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name '..'
2057: + lake init ....
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name '....'
2057: + lake init '  '
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name ''
2057: + lake init a/bc
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name 'a/bc'
2057: + lake init 'a\b'
2057: + grep --color 'illegal package name'
2057: + true
2057: error: illegal package name 'a\b'
2057: + lake init init
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake init Lean
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake init Lake
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake init main
2057: + grep --color 'reserved package name'
2057: + true
2057: error: reserved package name
2057: + lake new hello
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d hello exe hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built Hello.Basic
2057: ✔ [2/7] Built Hello
2057: ✔ [3/7] Built Hello.Basic:c.o
2057: ✔ [4/7] Built Main
2057: ✔ [5/7] Built Main:c.o
2057: ✔ [6/7] Built Hello:c.o
2057: ✔ [7/7] Built hello
2057: Hello, world!
2057: + test -f hello/.lake/build/lib/Hello.olean
2057: + rm -rf hello
2057: + lake new hello .toml
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d hello exe hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built Hello.Basic
2057: ✔ [2/7] Built Hello
2057: ✔ [3/7] Built Hello.Basic:c.o
2057: ✔ [4/7] Built Main
2057: ✔ [5/7] Built Main:c.o
2057: ✔ [6/7] Built Hello:c.o
2057: ✔ [7/7] Built hello
2057: Hello, world!
2057: + test -f hello/.lake/build/lib/Hello.olean
2057: + rm -rf hello
2057: + lake new hello exe
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + test -f hello/Main.lean
2057: + lake -d hello exe hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Main
2057: ✔ [2/3] Built Main:c.o
2057: ✔ [3/3] Built hello
2057: Hello, world!
2057: + rm -rf hello
2057: + lake new hello exe.toml
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + test -f hello/Main.lean
2057: + lake -d hello exe hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Main
2057: ✔ [2/3] Built Main:c.o
2057: ✔ [3/3] Built hello
2057: Hello, world!
2057: + rm -rf hello
2057: + lake new hello lib
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d hello build Hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Hello.Basic
2057: ✔ [2/3] Built Hello
2057: Build completed successfully.
2057: + test -f hello/.lake/build/lib/Hello.olean
2057: + rm -rf hello
2057: + lake new hello lib.toml
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d hello build Hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Hello.Basic
2057: ✔ [2/3] Built Hello
2057: Build completed successfully.
2057: + test -f hello/.lake/build/lib/Hello.olean
2057: + rm -rf hello
2057: + lake new qed math
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + sed_i '/^require.*/{N;d;}' qed/lakefile.lean
2057: + sed -i '' '/^require.*/{N;d;}' qed/lakefile.lean
2057: + lake -d qed build Qed
2057: info: qed: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Qed.Basic
2057: ✔ [2/3] Built Qed
2057: Build completed successfully.
2057: + test -f qed/.lake/build/lib/Qed.olean
2057: + rm -rf qed
2057: + lake new qed math.toml
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + sed_i '/^\[\[require\]\]/{N;N;N;d;}' qed/lakefile.toml
2057: + sed -i '' '/^\[\[require\]\]/{N;N;N;d;}' qed/lakefile.toml
2057: + lake -d qed build Qed
2057: info: qed: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Qed.Basic
2057: ✔ [2/3] Built Qed
2057: Build completed successfully.
2057: + test -f qed/.lake/build/lib/Qed.olean
2057: + mkdir hello
2057: + pushd hello
2057: ~/projects/lean4/src/lake/tests/init/hello ~/projects/lean4/src/lake/tests/init
2057: + lake init .
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake exe hello
2057: info: hello: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built Hello.Basic
2057: ✔ [2/7] Built Hello
2057: ✔ [3/7] Built Hello.Basic:c.o
2057: ✔ [4/7] Built Main
2057: ✔ [5/7] Built Main:c.o
2057: ✔ [6/7] Built Hello:c.o
2057: ✔ [7/7] Built hello
2057: Hello, world!
2057: + popd
2057: ~/projects/lean4/src/lake/tests/init
2057: + lake new HelloWorld
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d HelloWorld exe helloworld
2057: info: HelloWorld: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built HelloWorld.Basic
2057: ✔ [2/7] Built HelloWorld
2057: ✔ [3/7] Built HelloWorld.Basic:c.o
2057: ✔ [4/7] Built Main
2057: ✔ [5/7] Built Main:c.o
2057: ✔ [6/7] Built HelloWorld:c.o
2057: ✔ [7/7] Built helloworld
2057: Hello, world!
2057: + lake new hello.world
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d hello-world exe hello-world
2057: info: hello-world: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built Hello.World.Basic
2057: ✔ [2/7] Built Hello.World
2057: ✔ [3/7] Built Hello.World.Basic:c.o
2057: ✔ [4/7] Built Main
2057: ✔ [5/7] Built Main:c.o
2057: ✔ [6/7] Built Hello.World:c.o
2057: ✔ [7/7] Built «hello-world»
2057: Hello, world!
2057: + test -f hello-world/Hello/World/Basic.lean
2057: + lake new hello.exe exe
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d hello-exe exe hello-exe
2057: info: hello-exe: no previous manifest, creating one from scratch
2057: ✔ [1/3] Built Main
2057: ✔ [2/3] Built Main:c.o
2057: ✔ [3/3] Built «hello-exe»
2057: Hello, world!
2057: + lake new lean-data
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d lean-data exe lean-data
2057: info: lean-data: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built LeanData.Basic
2057: ✔ [2/7] Built LeanData
2057: ✔ [3/7] Built LeanData.Basic:c.o
2057: ✔ [4/7] Built LeanData:c.o
2057: ✔ [5/7] Built Main
2057: ✔ [6/7] Built Main:c.o
2057: ✔ [7/7] Built «lean-data»
2057: Hello, world!
2057: + lake new 123-hello
2057: warning: could not create a `lean-toolchain` file for the new package; no known toolchain name for the current Elan/Lean/Lake
2057: + lake -d 123-hello exe 123-hello
2057: info: 123-hello: no previous manifest, creating one from scratch
2057: ✔ [1/7] Built «123Hello».Basic
2057: ✔ [2/7] Built «123Hello»
2057: ✔ [3/7] Built Main
2057: ✔ [4/7] Built «123Hello».Basic:c.o
2057: ✔ [5/7] Built «123Hello»:c.o
2057: ✔ [6/7] Built Main:c.o
2057: ✔ [7/7] Built «123-hello»
2057: Hello, world!
2057: + '[' darwin23 '!=' msys ']'
2057: + lake new «A.B».«C.D»
2057: error: package already initialized
1/1 Test #2057: leanlaketest_init ................***Failed    9.86 sec