Repository navigation
Lean4Example error: build failed and Fail to use "suggest_tactics" #137
Description
0x01 Error messages
I followed your tutorial and deployed the lean-dojo/LeanCopilot and the LeanCopilot-demo branch of lean4-example on my server.There is still a compilation error, please help me to solve this problem. I find that a lot of people have this problem.Now I will explain my experimental environment and operation steps to you clearly.
error: Lean exited with code 132
Some required builds logged failures:
- Lean4Example
error: build failed0x02 Operating System environment
CPU: 8 cores
Memory: 32 GB
OS: Ubuntu-22.04
cmake version: 3.22.1
Ubuntu clang version: 14.0.0-1ubuntu1.1
arch: x86_64
lean4 version：Lean (version 4.11.0, x86_64-unknown-linux-gnu, commit ec3042d94bd1, Release)0x03 clone lean4-example
root@manjingliu-virtual-machine:~/demo# git clone -b LeanCopilot-demo https://github.com/yangky11/lean4-example.git
Cloning into 'lean4-example'...
remote: Enumerating objects: 514, done.
remote: Counting objects: 100% (146/146), done.
remote: Compressing objects: 100% (41/41), done.
remote: Total 514 (delta 115), reused 121 (delta 100), pack-reused 368 (from 2)
Receiving objects: 100% (514/514), 66.46 KiB | 199.00 KiB/s, done.
Resolving deltas: 100% (296/296), done.
root@manjingliu-virtual-machine:~/demo# ls
lean4-example
root@manjingliu-virtual-machine:~/demo# cd lean4-example/
root@manjingliu-virtual-machine:~/demo/lean4-example# ls
Dockerfile lakefile.lean lake-manifest.json Lean4Example.lean lean-toolchain LICENSE README.md0x04 lean-toolchain and lakefile.lean
1.lean-toolchain
root@manjingliu-virtual-machine:~/demo/lean4-example# cat lean-toolchain
leanprover/lean4:v4.11.02.lakefile.lean
root@manjingliu-virtual-machine:~/demo/lean4-example# cat lakefile.lean
import Lake
open Lake DSL
package «lean4-example» {
moreLinkArgs := #[
"-L./.lake/packages/LeanCopilot/.lake/build/lib",
"-lctranslate2"
]
}
@[default_target]
lean_lib «Lean4Example» {
}
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.6.0"0x05 lake update LeanCopilot
root@manjingliu-virtual-machine:~/demo/lean4-example# lake update LeanCopilot
info: downloading component 'lean'
200.9 MiB / 200.9 MiB (100 %) 10.8 MiB/s ETA: 0 s
info: installing component 'lean'
info: LeanCopilot: cloning https://github.com/lean-dojo/LeanCopilot.git to '././.lake/packages/LeanCopilot'
info: batteries: cloning https://github.com/leanprover-community/batteries.git to '././.lake/packages/batteries'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'0x06 lake exe LeanCopilot/download
root@manjingliu-virtual-machine:~/demo/lean4-example# lake exe LeanCopilot/download
ℹ [6/21] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j32`
ℹ [7/21] Replayed LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
info: Configuring CTranslate2 with `cmake -DOPENMP_RUNTIME=NONE -DWITH_MKL=OFF -DWITH_ACCELERATE=OFF -DWITH_OPENBLAS=ON -DOPENBLAS_INCLUDE_DIR=../../OpenBLAS -DOPENBLAS_LIBRARY=../../OpenBLAS/libopenblas.so ..`
info: Building CTranslate2 with `make -j32`
info: stdout:
[ 1%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/filesystem.c.o
[ 2%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/stack_line_reader.c.o
[ 3%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/string_view.c.o
[ 3%] Built target utils
[ 3%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_aarch64_linux_or_android.c.o
omit....
[ 96%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx512.cc.o
[ 97%] Linking CXX shared library libctranslate2.so
[ 97%] Built target ctranslate2
[ 98%] Building CXX object cli/CMakeFiles/translator.dir/translator.cc.o
[100%] Linking CXX executable ct2-translator
[100%] Built target translator
info: stderr:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc: In function ‘ctranslate2::cpu::GemmBackend ctranslate2::cpu::get_gemm_backend(ctranslate2::ComputeType)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc:51:18: warning: unused variable ‘is_int8’ [-Wunused-variable]
51 | const bool is_int8 = (compute_type == ComputeType::INT8
| ^~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc: In static member function ‘static void ctranslate2::primitives<D>::gemm(bool, bool, bool, bool, ctranslate2::dim_t, ctranslate2::dim_t, ctranslate2::dim_t, float, const In*, ctranslate2::dim_t, const In*, ctranslate2::dim_t, float, Out*, ctranslate2::dim_t, const Out*) [with In = signed char; Out = int; ctranslate2::Device D = ctranslate2::Device::CPU; ctranslate2::dim_t = long int]’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:43: warning: unused parameter ‘transpose_a’ [-Wunused-parameter]
881 | bool transpose_a, bool transpose_b,
| ~~~~~^~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:61: warning: unused parameter ‘transpose_b’ [-Wunused-parameter]
881 | bool transpose_a, bool transpose_b,
| ~~~~~^~~~~~~~~~~
omit...
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/layers/wav2vec2.h:30:28: warning: ‘ctranslate2::layers::Wav2Vec2LayerNormConvLayer::_transpose’ will be initialized after [-Wreorder]
30 | const ops::Transpose _transpose;
| ^~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/layers/wav2vec2.h:29:23: warning: ‘const ctranslate2::layers::LayerNorm ctranslate2::layers::Wav2Vec2LayerNormConvLayer::_output_norm’ [-Wreorder]
29 | const LayerNorm _output_norm;
| ^~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/layers/wav2vec2.cc:7:5: warning: when initialized here [-Wreorder]
7 | Wav2Vec2LayerNormConvLayer::Wav2Vec2LayerNormConvLayer(const models::Model& model,
| ^~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from /home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/layers/wav2vec2.cc:1:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/layers/wav2vec2.h: In constructor ‘ctranslate2::layers::Wav2Vec2Encoder::Wav2Vec2Encoder(const ctranslate2::models::Model&, const string&)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/layers/wav2vec2.h:91:19: warning: ‘ctranslate2::layers::Wav2Vec2Encoder::_num_heads’ will be initialized after [-Wreorder]
91 | const dim_t _num_heads;
| ^~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/layers/wav2vec2.h:89:28: warning: ‘const ctranslate2::ops::Transpose ctranslate2::layers::Wav2Vec2Encoder::_transpose’ [-Wreorder]
89 | const ops::Transpose _transpose;
| ^~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/layers/wav2vec2.cc:48:5: warning: when initialized here [-Wreorder]
48 | Wav2Vec2Encoder::Wav2Vec2Encoder(const models::Model& model, const std::string& scope)
| ^~~~~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/layers/wav2vec2.cc: In member function ‘void ctranslate2::layers::Wav2Vec2Encoder::operator()(const ctranslate2::StorageView&, ctranslate2::StorageView&)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/layers/wav2vec2.cc:84:27: warning: comparison of integer expressions of different signedness: ‘ctranslate2::dim_t’ {aka ‘long int’} and ‘std::vector<std::unique_ptr<const ctranslate2::layers::Wav2Vec2LayerNormConvLayer> >::size_type’ {aka ‘long unsigned int’} [-Wsign-compare]
84 | for (dim_t l = 0; l < _feat_layers.size(); l++) {
| ~~^~~~~~~~~~~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/layers/wav2vec2.cc:86:15: warning: comparison of integer expressions of different signedness: ‘ctranslate2::dim_t’ {aka ‘long int’} and ‘std::vector<std::unique_ptr<const ctranslate2::layers::Wav2Vec2LayerNormConvLayer> >::size_type’ {aka ‘long unsigned int’} [-Wsign-compare]
86 | if (l < _feat_layers.size() - 1 ) {
| ~~^~~~~~~~~~~~~~~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: In function ‘void ctranslate2::models::split_variables(ctranslate2::StorageView, int, std::vector<long int>&, std::vector<ctranslate2::StorageView>&)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:449:25: warning: comparison of integer expressions of different signedness: ‘int’ and ‘size_t’ {aka ‘long unsigned int’} [-Wsign-compare]
449 | for (int i = 0; i < num; ++i) {
| ~~^~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: In static member function ‘static std::shared_ptr<const ctranslate2::models::Model> ctranslate2::models::Model::load(ctranslate2::models::ModelReader&, ctranslate2::Device, int, ctranslate2::ComputeType, bool, bool)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:744:32: warning: comparison of integer expressions of different signedness: ‘std::vector<ctranslate2::StorageView>::size_type’ {aka ‘long unsigned int’} and ‘int’ [-Wsign-compare]
744 | if (outputs.size() > current_index && !outputs[current_index].empty())
| ~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:641:25: warning: unused variable ‘quantization_type’ [-Wunused-variable]
641 | QUANTIZATION_TYPE quantization_type = QUANTIZATION_TYPE::CT2;
| ^~~~~~~~~~~~~~~~~
In file included from /home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/ops/gemm.cc:1:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/ops/gemm.h: In constructor ‘ctranslate2::ops::Gemm::Gemm(float, float, bool, bool, bool, bool, const ctranslate2::ops::ActivationType*)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/ops/gemm.h:51:12: warning: ‘ctranslate2::ops::Gemm::_b_is_packed’ will be initialized after [-Wreorder]
51 | bool _b_is_packed;
| ^~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/include/ctranslate2/ops/gemm.h:43:29: warning: ‘const ctranslate2::ops::ActivationType* ctranslate2::ops::Gemm::_activation_type’ [-Wreorder]
43 | const ActivationType* _activation_type;
| ^~~~~~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/ops/gemm.cc:22:5: warning: when initialized here [-Wreorder]
22 | Gemm::Gemm(float alpha,
| ^~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: In function ‘ctranslate2::models::VARIABLE_TYPE ctranslate2::models::classify_variable(const string&)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:497:13: warning: this statement may fall through [-Wimplicit-fallthrough=]
497 | if (parameterName == "weight")
| ^~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:499:11: note: here
499 | default:
| ^~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:521:13: warning: this statement may fall through [-Wimplicit-fallthrough=]
521 | if (parameterName == "weight")
| ^~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:523:11: note: here
523 | default:
| ^~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:546:13: warning: this statement may fall through [-Wimplicit-fallthrough=]
546 | if (parameterName == "weight")
| ^~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:548:11: note: here
548 | default:
| ^~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: At global scope:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:455:17: warning: ‘bool ctranslate2::models::replace(std::string&, const string&, const string&)’ defined but not used [-Wunused-function]
455 | static bool replace(std::string& str, const std::string& from, const std::string& to) {
| ^~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: In static member function ‘static std::shared_ptr<const ctranslate2::models::Model> ctranslate2::models::Model::load(ctranslate2::models::ModelReader&, ctranslate2::Device, int, ctranslate2::ComputeType, bool, bool)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:744:34: warning: ‘current_index’ may be used uninitialized in this function [-Wmaybe-uninitialized]
744 | if (outputs.size() > current_index && !outputs[current_index].empty())
| ^~~~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:723:92: warning: ‘world_size’ may be used uninitialized in this function [-Wmaybe-uninitialized]
723 | dim_t dim_per_kqv_per_partition = SAFE_DIVIDE(variable.dim(outer_dim) / 2, world_size);
| ^~~~~~~~~~
ℹ [13/21] Replayed ModelCheckpointManager.Url
info: ././././ModelCheckpointManager/Url.lean:68:0: { protocol := "https", hostname := "huggingface.co", path := FilePath.mk "kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small" }
info: ././././ModelCheckpointManager/Url.lean:69:0: { protocol := "https", hostname := "huggingface.co", path := FilePath.mk "bert-base-uncased" }
info: ././././ModelCheckpointManager/Url.lean:71:0: "ct2-leandojo-lean4-tacgen-byt5-small"
info: ././././ModelCheckpointManager/Url.lean:72:0: "bert-base-uncased"
The model is available at /root/.cache/lean_copilot/models/huggingface.co/kaiyuy/ct2-byt5-small
The model is available at /root/.cache/lean_copilot/models/huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small
The model is available at /root/.cache/lean_copilot/models/huggingface.co/kaiyuy/premise-embeddings-leandojo-lean4-retriever-byt5-small
The model is available at /root/.cache/lean_copilot/models/huggingface.co/kaiyuy/ct2-leandojo-lean4-retriever-byt5-small
Done!0x07 lake build
root@manjingliu-virtual-machine:~/demo/lean4-example# lake build
ℹ [7/552] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j32`
ℹ [8/552] Replayed LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
info: Configuring CTranslate2 with `cmake -DOPENMP_RUNTIME=NONE -DWITH_MKL=OFF -DWITH_ACCELERATE=OFF -DWITH_OPENBLAS=ON -DOPENBLAS_INCLUDE_DIR=../../OpenBLAS -DOPENBLAS_LIBRARY=../../OpenBLAS/libopenblas.so ..`
info: Building CTranslate2 with `make -j32`
info: stdout:
[ 1%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/filesystem.c.o
[ 2%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/stack_line_reader.c.o
[ 3%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/string_view.c.o
[ 3%] Built target utils
omit...
[ 97%] Built target ctranslate2
[ 98%] Building CXX object cli/CMakeFiles/translator.dir/translator.cc.o
[100%] Linking CXX executable ct2-translator
[100%] Built target translator
info: stderr:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc: In function ‘ctranslate2::cpu::GemmBackend ctranslate2::cpu::get_gemm_backend(ctranslate2::ComputeType)’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc:51:18: warning: unused variable ‘is_int8’ [-Wunused-variable]
51 | const bool is_int8 = (compute_type == ComputeType::INT8
| ^~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc: In static member function ‘static void ctranslate2::primitives<D>::gemm(bool, bool, bool, bool, ctranslate2::dim_t, ctranslate2::dim_t, ctranslate2::dim_t, float, const In*, ctranslate2::dim_t, const In*, ctranslate2::dim_t, float, Out*, ctranslate2::dim_t, const Out*) [with In = signed char; Out = int; ctranslate2::Device D = ctranslate2::Device::CPU; ctranslate2::dim_t = long int]’:
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:43: warning: unused parameter ‘transpose_a’ [-Wunused-parameter]
881 | bool transpose_a, bool transpose_b,
| ~~~~~^~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:61: warning: unused parameter ‘transpose_b’ [-Wunused-parameter]
881 | bool transpose_a, bool transpose_b,
| ~~~~~^~~~~~~~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:44: warning: unused parameter ‘m’ [-Wunused-parameter]
882 | dim_t m, dim_t n, dim_t k,
| ~~~~~~^
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:53: warning: unused parameter ‘n’ [-Wunused-parameter]
882 | dim_t m, dim_t n, dim_t k,
| ~~~~~~^
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:62: warning: unused parameter ‘k’ [-Wunused-parameter]
882 | dim_t m, dim_t n, dim_t k,
| ~~~~~~^
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:883:44: warning: unused parameter ‘alpha’ [-Wunused-parameter]
883 | float alpha,
| ~~~~~~^~~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:52: warning: unused parameter ‘a’ [-Wunused-parameter]
884 | const int8_t* a, dim_t lda,
| ~~~~~~~~~~~~~~^
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:61: warning: unused parameter ‘lda’ [-Wunused-parameter]
884 | const int8_t* a, dim_t lda,
| ~~~~~~^~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:52: warning: unused parameter ‘b’ [-Wunused-parameter]
885 | const int8_t* b, dim_t ldb,
| ~~~~~~~~~~~~~~^
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:61: warning: unused parameter ‘ldb’ [-Wunused-parameter]
885 | const int8_t* b, dim_t ldb,
| ~~~~~~^~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:886:44: warning: unused parameter ‘beta’ [-Wunused-parameter]
886 | float beta,
| ~~~~~~^~~~
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:47: warning: unused parameter ‘c’ [-Wunused-parameter]
887 | int32_t* c, dim_t ldc,
| ~~~~~~~~~^
/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:56: warning: unused parameter ‘ldc’ [-Wunused-parameter]
887 | int32_t* c, dim_t ldc,
| ~~~~~~^~~
omit...
info: ././././ModelCheckpointManager/Url.lean:71:0: "ct2-leandojo-lean4-tacgen-byt5-small"
info: ././././ModelCheckpointManager/Url.lean:72:0: "bert-base-uncased"
✖ [551/552] Building Lean4Example
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib /root/.elan/toolchains/leanprover--lean4---v4.11.0/bin/lean ././././Lean4Example.lean -R ./././. -o ././.lake/build/lib/Lean4Example.olean -i ././.lake/build/lib/Lean4Example.ilean -c ././.lake/build/ir/Lean4Example.c --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Url-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Download-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Native-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-ByT5-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Builtin-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Interface-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-External-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Generic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-FFI-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-AssocList-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-SatisfiesM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Monadic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-WF-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Registry-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Options-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-MLList-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-Nondet-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Frontend-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnionFind-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-Order-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-UInt-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Char-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Match-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Matcher-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashMap-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-DiscrTree-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Tactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RulePattern-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Public-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Internal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Percent-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-FVarIdSubst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-GoalDiff-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-CtorNames-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-MonadBacktrack-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-SavedState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-EqualUpToIds-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-GoalWithMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-TacticState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Util-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-PermuteGoals-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Step-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-InstantiateMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Member-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Filter-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-Init-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-ElabM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-ElabRuleTerm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Apply-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-OpenPrivate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-ScriptM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Clear-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Inaccessible-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SpecificTactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Cases-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Cases-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Constructors-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-NormSimp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Default-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-RuleExpr-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Attribute-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScriptToSScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureDynamic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureStatic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-OptimizeSyntax-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Apply-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-UnusedNames-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-AssertHypotheses-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Preprocess-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Simp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Constants-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-UnsafeQueue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Data-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Traversal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-RunMetaM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-TreeM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-AddRapp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-State-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-HashSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractProof-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Free-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-Class-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-SearchM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-RuleSelection-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Norm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Exception-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-ExpandSafePrefix-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-BinomialHeap-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Assumption-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-ApplyHyps-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-DestructProducts-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Intros-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Rfl-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Split-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Subst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Report-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Command-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-LlmAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-1.so --json
error: Lean exited with code 132
Some required builds logged failures:
- Lean4Example
error: build failed0x08 final error message
Part 8 is the error message at the end of Part 7
✖ [551/552] Building Lean4Example
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib /root/.elan/toolchains/leanprover--lean4---v4.11.0/bin/lean ././././Lean4Example.lean -R ./././. -o ././.lake/build/lib/Lean4Example.olean -i ././.lake/build/lib/Lean4Example.ilean -c ././.lake/build/ir/Lean4Example.c --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Url-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Download-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Native-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-ByT5-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Builtin-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Interface-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-External-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Generic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-FFI-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-AssocList-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-SatisfiesM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Monadic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-WF-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Registry-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Options-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-MLList-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-Nondet-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Frontend-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnionFind-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-Order-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-UInt-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Char-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Match-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Matcher-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashMap-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-DiscrTree-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Tactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RulePattern-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Public-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Internal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Percent-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-FVarIdSubst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-GoalDiff-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-CtorNames-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-MonadBacktrack-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-SavedState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-EqualUpToIds-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-GoalWithMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-TacticState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Util-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-PermuteGoals-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Step-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-InstantiateMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Member-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Filter-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-Init-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-ElabM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-ElabRuleTerm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Apply-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-OpenPrivate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-ScriptM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Clear-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Inaccessible-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SpecificTactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Cases-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Cases-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Constructors-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-NormSimp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Default-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-RuleExpr-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Attribute-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScriptToSScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureDynamic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureStatic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-OptimizeSyntax-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Apply-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-UnusedNames-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-AssertHypotheses-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Preprocess-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Simp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Constants-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-UnsafeQueue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Data-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Traversal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-RunMetaM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-TreeM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-AddRapp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-State-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-HashSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractProof-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Free-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-Class-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-SearchM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-RuleSelection-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Norm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Exception-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-ExpandSafePrefix-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-BinomialHeap-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Assumption-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-ApplyHyps-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-DestructProducts-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Intros-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Rfl-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Split-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Subst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Report-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Command-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-LlmAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-1.so --json
error: Lean exited with code 132
Some required builds logged failures:
- Lean4Example
error: build failed
Activity
[-]Lean4Example error: build failed[/-][+]Lean4Example error: build failed and Fail to use "suggest_tactics" [/+]zzhisthebest commentedon Dec 24, 2024
We meet the same error,and I still don't solve it.
yangky11 commentedon Dec 25, 2024
I updated LeanCopilot to support recent versions of Lean. Could you please re-try and see if the error still persists?
6AlexMan commentedon Dec 26, 2024
I have re-try,but the error still persists.☹️
✖ [556/557] Building Lean4Example trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib :././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aeso p/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib /root/.elan/toolchains/leanprover--lean4---v4.14.0/bin/lean ././././Lean4Example.lean - R ./././. -o ././.lake/build/lib/Lean4Example.olean -i ././.lake/build/lib/Lean4Example.ilean -c ././.lake/build/ir/Lean4Example.c --load-dynlib=././.la ke/packages/LeanCopilot/.lake/build/lib/libleanffi.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Url-1.so -- load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Download-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/bu ild/lib/libModelCheckpointManager-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Native-1.so --load-dynlib=././ .lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-ByT5-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-M odels-Builtin-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Interface-1.so --load-dynlib=././.lake/packages/Le anCopilot/.lake/build/lib/libLeanCopilot-Models-External-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Generic -1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-FFI-1.so --load-dynlib=././.lake/packages/batteries/.lake/build /lib/libBatteries-Data-List-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.so --load-dynlib= ././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries- CodeAction-Deprecated-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.so --load-dynlib=././.lake/packages/ba tteries/.lake/build/lib/libBatteries-Data-List-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-AssocList-1.so -- load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/lib Batteries-Lean-EStateM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Except-1.so --load-dynlib=././.lake/packages/ba tteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.s o --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-OpenPrivate-1.so --load-dynlib=././.lake/packages/batteries/.lake/build /lib/libBatteries-Util-LibraryNote-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Simp-1.so --load-dynlib=././ .lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-TypeClass-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries -Tactic-Lint-Frontend-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-1.so --load-dynlib=././.lake/packages/bat teries/.lake/build/lib/libBatteries-Classes-SatisfiesM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Monadic-1 .so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/bui ld/lib/libBatteries-Data-HashMap-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.so --load-dynlib= ././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-C ontrol-ForInStep-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Lemmas-1.so --load-dynlib=././.lak e/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Lem mas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-WF-1.so --load-dynlib=././.lake/packages/batteries/.lake/b uild/lib/libBatteries-Data-HashMap-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Registry-1.so --load-dynlib=. /./.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Opt ions-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-MLList-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lak e/build/lib/libBatteries-Control-Nondet-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Frontend-1.so --load-dynl ib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge -1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build /lib/libBatteries-Lean-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.so --load-dynlib=././.lake/ packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Match-1.so -- load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Matcher-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/ lib/libLeanCopilot-Tactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/ build/lib/libAesop-Options-Public-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Internal-1.so --load-dynlib=././.lake/pac kages/aesop/.lake/build/lib/libAesop-Options-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Name-1.so --load-dynlib=././.lake /packages/batteries/.lake/build/lib/libBatteries-Data-Array-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Dat a-Array-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/l ibAesop-RulePattern-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/b uild/lib/libAesop-Percent-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-FVarIdSubst-1.so --load-dynlib=././.lake/packages /aesop/.lake/build/lib/libAesop-RuleTac-GoalDiff-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-CtorNames-1.so --load-dynli b=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Eq ualUpToIds-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/li b/libAesop-Script-GoalWithMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-TacticState-1.so --load-dynlib=././.lake/pac kages/batteries/.lake/build/lib/libBatteries-Lean-MonadBacktrack-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta- SavedState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Util-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/ lib/libBatteries-Tactic-PermuteGoals-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Step-1.so --load-dynlib=././.lake/packa ges/aesop/.lake/build/lib/libAesop-RuleTac-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Basic-1.so --load-dynlib=././ .lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-InstantiateMVars-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatt eries-Lean-PersistentHashSet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Expr-1.so --load-dynlib=././.lake/pa ckages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashMap-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-M eta-DiscrTree-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/lib Aesop-RuleSet-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Filter-1.so --load-dynlib=././.lake/packages/aesop/.lake /build/lib/libAesop-Rule-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Member-1.so --load-dynlib=././.lake/packages/aesop /.lake/build/lib/libAesop-RuleSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScript-1.so --load-dynlib=././.lake/packa ges/aesop/.lake/build/lib/libAesop-Script-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SScript-1.so --load-dynlib=. /./.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScriptToSScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Str uctureDynamic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureStatic-1.so --load-dynlib=././.lake/packages/aesop/.l ake/build/lib/libAesop-Script-OptimizeSyntax-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Basic-1.so --load-dynlib=././.la ke/packages/aesop/.lake/build/lib/libAesop-Script-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-ElabM-1.so --load-dynlib=./. /.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-ElabRuleTerm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-1.s o --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-U til-Tactic-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-ScriptM-1.so --load-dynlib=././.lake/packages/batteries/.l ake/build/lib/libBatteries-Lean-Meta-Inaccessible-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SpecificTactics-1.so --loa d-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Apply-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Ca ses-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-UnusedNames-1.so --load-dynlib=././.lake/packages/aesop/.lake /build/lib/libAesop-RuleTac-Forward-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-1.so --load-dynlib=././.l ake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Preprocess-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expa nsion-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Simp-1.so --load-dynlib=././.lake/packages/aesop/.lake /build/lib/libAesop-Constants-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-UnsafeQueue-1.so --load-dynlib=././.lake/package s/aesop/.lake/build/lib/libAesop-Tree-Data-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-RunMetaM-1.so --load-dynlib=././.la ke/packages/aesop/.lake/build/lib/libAesop-Search-Queue-Class-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-TreeM-1.so --loa d-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-SearchM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Ru leSelection-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Traversal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/ lib/libAesop-Tree-State-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-HashSet-1.so --load-dynlib=././.lake/packages/ aesop/.lake/build/lib/libAesop-Search-Expansion-Norm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnionFind-1.so --load-dyn lib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-AddRapp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion -1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Exception-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Sea rch-ExpandSafePrefix-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/b uild/lib/libAesop-Tree-ExtractProof-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractScript-1.so --load-dynlib=././.lake /packages/aesop/.lake/build/lib/libAesop-Tree-Free-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Tracing-1.so --load-dynlib= ././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-Order-1.so - -load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-BinomialHeap-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/l ib/libAesop-Search-Queue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-Init-1.so --load-dynlib=././.lake/packa ges/aesop/.lake/build/lib/libAesop-Frontend-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Main-1.so --load-dynli b=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Cases-1.s o --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Constructors-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAe sop-Builder-NormSimp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.la ke/build/lib/libAesop-Builder-Apply-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Default-1.so --load-dynlib=././.lake/pa ckages/aesop/.lake/build/lib/libAesop-Builder-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Unfold-1.so --load-dy nlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-RuleExpr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Ta ctic-Unreachable-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Linter-UnreachableTactic-1.so --load-dynlib=././.lake/pack ages/aesop/.lake/build/lib/libAesop-Frontend-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Extension-1.so --load-dyn lib=././.lake/packages/aesop/.lake/build/lib/libAesop-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Basic-1.so --lo ad-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Report-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-C ommand-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAeso p-Frontend-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Attribute-1.so --load-dynlib=././.lake/packages/aesop/ .lake/build/lib/libAesop-BuiltinRules-Assumption-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-ApplyHyps-1.so --load -dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-DestructProducts-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libA esop-BuiltinRules-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Intros-1.so --load-dynlib=././.lake/packages/aes op/.lake/build/lib/libAesop-BuiltinRules-Rfl-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Split-1.so --load-dynlib= ././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Subst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-1 .so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Llm Aesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-1.so --json error: Lean exited with code 132 Some required builds logged failures: - Lean4Example error: build failed6AlexMan commentedon Dec 26, 2024
Can you try it with Ubuntu22.04 Linux? I think it's a way to reproduce bugs.
Peiyang-Song commentedon Jan 4, 2025
Hi @6AlexMan , thank you for the additional report. I just retried the latest version of Lean Copilot on my Ubuntu 22.04 Linux but was not able to produce your issue. Both the source Lean Copilot repo and the Lean4Example repo successfully built (I believe Ubuntu Linux is included in the CI tests too which also succeeded). I would open up a fresh environment and follow the exact steps that worked on CI/build scripts to retry.
6AlexMan commentedon Jan 7, 2025
Thank you for your reply. I have reinstalled Ubuntu22.04, and the system environment is relatively clean. Many other questioners should have had the same problem as me.
zzhisthebest commentedon Jan 10, 2025
@6AlexMan Have you solved it?It is really annoying. :-(
6AlexMan commentedon Jan 10, 2025
The problem has not been solved
UlrikBuchholtz commentedon Jul 23, 2025
I also get this issue (using the current LeanCopilot-demo branch here.
lake buildfails witherror: Lean exited with code 132and a call tosuggest_tacticsin vscode givesServer process for file:///home/ulrik/src/lean4-example/Lean4Example.lean crashed, likely due to a stack overflow or a bug.– Let me know if you need more information.pyscriptor commentedon Jul 28, 2025
error: Lean exited with code 132
Some required builds logged failures:
error: build failed
mohrm commentedon Jul 30, 2025
Hi!
I can confirm the behaviour und could track it down further. My explaination goes as follows:
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v4.16.0"and run
lake build, this will not just clone LeanCopilot and build it. It will look for a prebuilt artifact that supposedly fits the architecture ("x86_64"), download it and just use that.Actually, this can be seen in the log cited in the first message of @6AlexMan: It contains lines like
and I'm pretty sure that the home directory of @6AlexMan is not /home/peiyangsong.
cc -O2 -DSMALL_MATRIX_OPT -DMAX_STACK_ALLOC=2048 -DEXPRECISION -m128bit-long-double -Wall -m64 -DF_INTERFACE_GFORT -fPIC -DC_LAPACK -DNO_LAPACK -DNO_LAPACKE -DSMP_SERVER -DNO_WARMUP -DMAX_CPU_NUMBER=128 -DMAX_PARALLEL_NUMBER=1 -DBUILD_SINGLE=1 -DBUILD_DOUBLE=1 -DBUILD_COMPLEX=1 -DBUILD_COMPLEX16=1 -DVERSION=\"0.3.29.dev\" -msse3 -mssse3 -msse4.1 -mavx -mavx2 -march=cooperlake -mavx2 -UASMNAME -UASMFNAME -UNAME -UCNAME -UCHAR_NAME -UCHAR_CNAME -DASMNAME=dgemm_small_kernel_b0_tt -DASMFNAME=dgemm_small_kernel_b0_tt_ -DNAME=dgemm_small_kernel_b0_tt_ -DCNAME=dgemm_small_kernel_b0_tt -DCHAR_NAME=\"dgemm_small_kernel_b0_tt_\" -DCHAR_CNAME=\"dgemm_small_kernel_b0_tt\" -DNO_AFFINITY -I.. -DDOUBLE -UCOMPLEX -c -DDOUBLE -UCOMPLEX -DB0 ../kernel/x86_64/dgemm_small_kernel_tt_skylakex.c -o dgemm_small_kernel_b0_tt.oPlease note the "-march=cooperlake". OpenBLAS has some built-in magic that determines instructions that the CPU on your machine has available and the machine @Peiyang-Song to build LeanCopilot apparently has a cooperlake CPU. Why is this relevant? Because cooperlake CPUs support AVX-512 instructions which the compiler happily emits to obtain the library.
So, we can conclude that the prebuilt artifact that @Peiyang-Song provides via github and that everyone who tries to build Lean4Example uses contains native libraries that are only supported by CPUs that have AVX-512 instructions available.
Now, I also observed the 132 error of lean with the last command. So, I ran it in gdb and could confirm that the program crashes on the first encounter of an AVX-512 instruction.
`pythi@...:~/Projects/lean4/lean4-example$ LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib gdb --args /home/pythi/.elan/toolchains/leanprover--lean4---v4.16.0/bin/lean ././././Lean4Example.lean -R ./././. -o ././.lake/build/lib/Lean4Example.olean -i ././.lake/build/lib/Lean4Example.ilean -c ././.lake/build/ir/Lean4Example.c --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Url-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Download-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Native-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-ByT5-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Builtin-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Interface-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-External-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Generic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-FFI-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-AssocList-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-EStateM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Except-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-OpenPrivate-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Util-LibraryNote-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Simp-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-TypeClass-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Frontend-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-SatisfiesM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Monadic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-WF-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Registry-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Options-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-MLList-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-Nondet-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Frontend-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-DiscrTreeConfig-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Match-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Matcher-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Tactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Public-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Internal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Name-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RulePattern-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Percent-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-FVarIdSubst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-GoalDiff-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-CtorNames-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-EqualUpToIds-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-GoalWithMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-TacticState-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-MonadBacktrack-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-SavedState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Util-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-PermuteGoals-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Step-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-InstantiateMVars-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashSet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashMap-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-DiscrTree-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Filter-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Member-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScriptToSScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureDynamic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureStatic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-OptimizeSyntax-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-ElabM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-ElabRuleTerm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-ScriptM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Inaccessible-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SpecificTactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Apply-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Cases-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-UnusedNames-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Preprocess-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Simp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Constants-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-UnsafeQueue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Data-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-RunMetaM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-Class-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-TreeM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-SearchM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-RuleSelection-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Traversal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-State-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-HashSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Norm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnionFind-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-AddRapp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Exception-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-ExpandSafePrefix-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractProof-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Free-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-Order-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-BinomialHeap-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-Init-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Cases-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Constructors-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-NormSimp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Apply-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Default-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-RuleExpr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Unreachable-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Linter-UnreachableTactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Report-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Command-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Attribute-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Assumption-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-ApplyHyps-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-DestructProducts-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Intros-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Rfl-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Split-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Subst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-LlmAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-1.so --json
GNU gdb (Debian 13.1-3) 13.1
Copyright (C) 2023 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later http://gnu.org/licenses/gpl.html
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
https://www.gnu.org/software/gdb/bugs/.
Find the GDB manual and other documentation resources online at:
http://www.gnu.org/software/gdb/documentation/.
For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from /home/pythi/.elan/toolchains/leanprover--lean4---v4.16.0/bin/lean...
(gdb) run
Starting program: /home/pythi/.elan/toolchains/leanprover--lean4---v4.16.0/bin/lean ././././Lean4Example.lean -R ./././. -o ././.lake/build/lib/Lean4Example.olean -i ././.lake/build/lib/Lean4Example.ilean -c ././.lake/build/ir/Lean4Example.c --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Url-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Download-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Native-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-ByT5-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Builtin-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Interface-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-External-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Generic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-FFI-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-AssocList-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-EStateM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Except-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-OpenPrivate-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Util-LibraryNote-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Simp-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-TypeClass-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Frontend-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-SatisfiesM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Monadic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-WF-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Registry-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Options-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-MLList-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-Nondet-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Frontend-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-DiscrTreeConfig-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Match-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Matcher-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Tactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Public-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-Internal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Options-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Name-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RulePattern-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Percent-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-FVarIdSubst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-GoalDiff-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-CtorNames-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-EqualUpToIds-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-GoalWithMVars-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-TacticState-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-MonadBacktrack-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-SavedState-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Util-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-PermuteGoals-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Step-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-InstantiateMVars-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashSet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-PersistentHashMap-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-DiscrTree-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Index-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Name-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Filter-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Rule-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-Member-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-UScriptToSScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureDynamic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-StructureStatic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-OptimizeSyntax-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-ElabM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-ElabRuleTerm-1.so --load---Type for more, q to quit, c to continue without paging--
dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Tactic-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-ScriptM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-Inaccessible-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Script-SpecificTactics-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Apply-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Cases-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Meta-UnusedNames-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Preprocess-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-RuleTac-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Simp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Constants-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-UnsafeQueue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Data-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-RunMetaM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-Class-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-TreeM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-SearchM-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-RuleSelection-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Traversal-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-State-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-HashSet-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-Norm-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnionFind-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-AddRapp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Expansion-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Exception-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-ExpandSafePrefix-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Check-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractProof-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractScript-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Free-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-Tracing-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-Order-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-BinomialHeap-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Queue-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-Init-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Search-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Cases-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Constructors-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-NormSimp-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Apply-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Default-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Forward-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Builder-Unfold-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-RuleExpr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Unreachable-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Linter-UnreachableTactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Tactic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Extension-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Main-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Stats-Report-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Command-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Saturate-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Frontend-Attribute-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Assumption-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-ApplyHyps-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-DestructProducts-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Ext-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Intros-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Rfl-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Split-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-Subst-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-BuiltinRules-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-LlmAesop-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-1.so --json
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
[New Thread 0x7fffafdff6c0 (LWP 22522)]
[New Thread 0x7fffaf5fe6c0 (LWP 22523)]
[New Thread 0x7fffaedfd6c0 (LWP 22524)]
[New Thread 0x7fffae5fc6c0 (LWP 22525)]
[New Thread 0x7fffaddfb6c0 (LWP 22526)]
[New Thread 0x7fffad5fa6c0 (LWP 22527)]
[New Thread 0x7fffacdf96c0 (LWP 22528)]
[New Thread 0x7fffab9ea6c0 (LWP 22529)]
[New Thread 0x7fffa3fff6c0 (LWP 22530)]
[New Thread 0x7fff9bfff6c0 (LWP 22531)]
[New Thread 0x7fffa37fe6c0 (LWP 22532)]
[Thread 0x7fffacdf96c0 (LWP 22528) exited]
[Thread 0x7fffad5fa6c0 (LWP 22527) exited]
[Thread 0x7fffaddfb6c0 (LWP 22526) exited]
[Thread 0x7fffae5fc6c0 (LWP 22525) exited]
[Thread 0x7fffaedfd6c0 (LWP 22524) exited]
[Thread 0x7fffaf5fe6c0 (LWP 22523) exited]
[Thread 0x7fffafdff6c0 (LWP 22522) exited]
[Detaching after fork from child process 22533]
[New Thread 0x7fffacdf96c0 (LWP 22534)]
[Thread 0x7fffacdf96c0 (LWP 22534) exited]
[Detaching after fork from child process 22541]
[New Thread 0x7fffacdf96c0 (LWP 22542)]
[Thread 0x7fffacdf96c0 (LWP 22542) exited]
[Detaching after fork from child process 22543]
[New Thread 0x7fffacdf96c0 (LWP 22544)]
[Thread 0x7fffacdf96c0 (LWP 22544) exited]
[New Thread 0x7fffacdf96c0 (LWP 22545)]
[New Thread 0x7fffad5fa6c0 (LWP 22546)]
[New Thread 0x7fffaddfb6c0 (LWP 22547)]
[New Thread 0x7fffae5fc6c0 (LWP 22548)]
[New Thread 0x7fff98fbc6c0 (LWP 22549)]
[New Thread 0x7fff4d5ad6c0 (LWP 22550)]
[New Thread 0x7fff4cdac6c0 (LWP 22551)]
[New Thread 0x7fff37fff6c0 (LWP 22552)]
[New Thread 0x7fff377fe6c0 (LWP 22553)]
[New Thread 0x7fff36ffd6c0 (LWP 22554)]
[New Thread 0x7fff367fc6c0 (LWP 22555)]
[New Thread 0x7fff35ffb6c0 (LWP 22556)]
Thread 27 "lean" received signal SIGILL, Illegal instruction.
[Switching to Thread 0x7fff35ffb6c0 (LWP 22556)]
0x00007ffff05a1a7c in sgemm_beta () from ././.lake/packages/LeanCopilot/.lake/build/lib/libopenblas.so.0
(gdb) x/10i $rip
=> 0x7ffff05a1a7c <sgemm_beta+188>: vmovups %zmm0,(%rax)
0x7ffff05a1a82 <sgemm_beta+194>: vmovups %zmm0,0x40(%rax)
0x7ffff05a1a89 <sgemm_beta+201>: sub $0xffffffffffffff80,%rax
0x7ffff05a1a8d <sgemm_beta+205>: cmp $0x1f,%rdx
0x7ffff05a1a91 <sgemm_beta+209>: jg 0x7ffff05a1a78 <sgemm_beta+184>
0x7ffff05a1a93 <sgemm_beta+211>: mov (%rsp),%rax
0x7ffff05a1a97 <sgemm_beta+215>: add 0x8(%rsp),%rdi
0x7ffff05a1a9c <sgemm_beta+220>: cmp $0x7,%rax
0x7ffff05a1aa0 <sgemm_beta+224>: jle 0x7ffff05a1ae1 <sgemm_beta+289>
0x7ffff05a1aa2 <sgemm_beta+226>: lea -0x8(%rax),%r13
(gdb)`
In contrast, when I change the require-clause in the lakefile.lean to
require LeanCopilot from git "../LeanCopilot" @ "v4.16.0"and run the build, it actually builds LeanCopilot for my machine and then it just works :-)
Although it is just my machine, I am relatively convinced that this is indeed the cause for the issue. Why?
In conclustion, I think that it is fine if the prebuilt artifact requires special hardware but this should be made crystal clear so that there are no bad surprises.
It should be made clear in the documentation that the provided github artefact can only be used if the CPU on one's machine supports AVX-512. If the CPU doesn't, one should use a modified lakefile.lean (as I showed).
I hope that my contribution was of some help.
6AlexMan commentedon Jul 30, 2025
Thanks for your reply
Thanks for your reply
Peiyang-Song commentedon Aug 5, 2025
Thank you @mohrm so much for the contribution! This is all very helpful. We are looking into your analysis and will update the documentation accordingly afterward. Thanks again!
ide-developer commentedon Aug 16, 2026
Confirming this is still present and reproducible on the current release,
v4.31.0(commit2458f7339df4d90643cdc6eb3fbbe968cd73ac78), and independently landing on the exact same root cause @mohrm already diagnosed above — the bundled OpenBLAS artifact is compiled-march=cooperlake(AVX-512), and itSIGILLs on any CPU without AVX-512. Adding this because it reproduces on real bare-metal hardware (not a VM, unlike the earlier reports in this thread), which rules out any theory that this is a hypervisor CPUID-passthrough quirk rather than a genuine target mismatch in the shipped artifact.Summary
lake buildsuggest_tacticsLean exited with code 132(SIGILL)✅ Passing environment — macOS / Apple Silicon
4.32.0-rc1via elan (the toolchainv4.31.0'slean-toolchainpins)lakefile.lean's owngetBuildFlags(line 279), macOS builds CTranslate2 with-DWITH_ACCELERATE=ON -DWITH_OPENBLAS=OFF— it never touches the x86 OpenBLAS SIMD kernels at all, which is presumably exactly why this platform is unaffected.suggest_tacticson a trivial goal:❌ Failing environment — Linux, bare-metal Haswell
avx avx2 fma— noavx512*flags at all6.8.4-200.fc39.x86_644.32.0-rc1via elan (same toolchain as macOS)lake buildreports success, but per the Lake trace log it doesn't compile OpenBLAS on this machine at all — it fetches a prebuilt artifact:/home/peiyangsong/LeanCopilot/...as the build path — the exact same phenomenon @mohrm diagnosed above, confirmed still present in the current release, on completely different (and this time, definitely-physical) hardware.libopenblas_cooperlakep-r0.3.33.dev.a, and the shippedlibopenblas.so.0embeds the build tagOpenBLAS 0.3.33.dev NO_LAPACK NO_LAPACKE NO_AFFINITY COOPERLAKE.💥 Crash evidence — coredump + disassembly
suggest_tactics(and anylake buildthat elaborates a file importingLeanCopilot) reliably crashes theleanprocess:Disassembling
libopenblas.so.0at the crashing offset lands squarely insidesgemm_beta— the same function @mohrm's analysis pointed at:%zmm0is a 512-bit AVX-512 register — this CPU has no AVX-512 support of any kind, henceSIGILL.Why add this
v4.31.0, and now reproduced on real bare-metal hardware rather than a VM.lake buildtrace log / coredump if useful for a fix (e.g.DYNAMIC_ARCH=1,TARGET=per-arch release artifacts, or a runtime CPUID guard before calling into the OpenBLAS SIMD kernels).ide-developer commentedon Aug 16, 2026
Context for anyone landing on this comment directly (click to expand)
This follows up on #137 itself: LeanCopilot's shipped OpenBLAS release artifact is compiled
-march=cooperlake(AVX-512), sosuggest_tactics/anything that loads it crashes withSIGILLon any CPU without AVX-512 (e.g. Haswell). See my previous comment for the disassembly/coredump evidence. This comment adds a workaround that unblocks it without touching LeanCopilot's own source.Workaround that works (tested), for anyone hitting this on Haswell-class or otherwise pre-AVX-512 x86_64 hardware
Since the crash is caused by the shipped OpenBLAS artifact being compiled
-march=cooperlake/AVX-512 (not by anything in your own project), you can swap it out for any correctly-targeted OpenBLAS build afterlake buildhas fetched/unpacked LeanCopilot, without touching LeanCopilot's own source:Verified on the same real bare-metal Xeon E5-2640 v3 ("Haswell") box from my comment above:
suggest_tacticsreliablySIGILLs (Lean exited with code 132), every time, andcoredumpctlshows it crashing at thevmovups %zmm0,...instruction insidelibopenblas.so.0'ssgemm_beta(see the disassembly in my earlier comment).openblas-serial-0.3.21-6.fc39.x86_64'slibopenblas.so.0(sameSONAME libopenblas.so.0, so no relinking needed — just drop-in replace the file): two separate cleanlake build <YourLib>runs both completed successfully, one showingBuilt LeancopilotDemoPkg.Basic (10s)(a genuine fresh model-inference run, ~10s — not a cached replay) and correctly printing:coredumpctl listacross either post-swap run.Caveats:
lakefile.lean— it'll need repeating after anylake clean/freshlake update LeanCopilot.openblas-serial, non-threaded) exports a strict superset of the symbols the bundledNO_LAPACK=1 NO_FORTRAN=1build does (17196 vs. 3188 exported symbols), so nothing appears to be missing for CTranslate2's needs — but I only exercised thesuggest_tactics/premise-selection path shown above, not the full test suite.DYNAMIC_ARCH=1(OpenBLAS's own runtime-CPUID dispatch) instead of a single fixed-march=, or publishing per-microarchitecture release artifacts — but this at least unblocks anyone stuck on older/non-AVX-512 hardware today.Fix OpenBLAS SIGILL, lean_exe libstdc++ link failure, and pin native …
Peiyang-Song commentedon Aug 18, 2026
Fixed in #195. Thanks for the thorough diagnosis and for everyone's inputs to the discussion.
The fix builds OpenBLAS with DYNAMIC_ARCH=1, so the shipped release artifact embeds kernels for multiple x86_64/arm64 microarchitectures and dispatches between them at runtime via CPUID, instead of hardcoding whatever ISA extensions happen to be available on the CI machine that builds it (which is how it ended up -march=cooperlake/AVX-512-only). This should also make the manual OpenBLAS-swap workaround posted above unnecessary going forward.
Closing this as a result.