Lean4Example error: build failed and Fail to use "suggest_tactics"

[6AlexMan]

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 failed

0x02 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.md

0x04 lean-toolchain and lakefile.lean

1.lean-toolchain

root@manjingliu-virtual-machine:~/demo/lean4-example# cat lean-toolchain 
leanprover/lean4:v4.11.0

2.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 failed

0x08 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

[zzhisthebest]

We meet the same error,and I still don't solve it.

[yangky11]

I updated LeanCopilot to support recent versions of Lean. Could you please re-try and see if the error still persists?

[6AlexMan]

I updated LeanCopilot to support recent versions of Lean. Could you please re-try and see if the error still persists?

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 failed                              

[6AlexMan]

I updated LeanCopilot to support recent versions of Lean. Could you please re-try and see if the error still persists?

Can you try it with Ubuntu22.04 Linux? I think it's a way to reproduce bugs.

[Peiyang-Song]

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]

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]

@6AlexMan Have you solved it?It is really annoying. :-(

[6AlexMan]

@6AlexMan Have you solved it?It is really annoying. :-(

The problem has not been solved

[UlrikBuchholtz]

I also get this issue (using the current LeanCopilot-demo branch here. lake build fails with error: Lean exited with code 132 and a call to suggest_tactics in vscode gives Server 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]

error: Lean exited with code 132
Some required builds logged failures:

• Project1
  error: build failed

[mohrm]

Hi!
I can confirm the behaviour und could track it down further. My explaination goes as follows:

• Lake/Lean make great use of caching and prebuilt binaries. If I have in my lakefile.lean a line like
  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.
• The build log in this case does not actually compile anything in LeanCopilot but rather replay the logs that were gathered during the actual build.
  Actually, this can be seen in the log cited in the first message of @6AlexMan: It contains lines like

/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc: In function

and I'm pretty sure that the home directory of @6AlexMan is not /home/peiyangsong.

• Hence, we can conclude that @Peiyang-Song provided a prebuilt artifact and if others follow the instruction4 for the lean4-example, their build will download that prebuilt artifact.
• Also note that the prebuilt artifact does not only contain LeanCopilot itself but also various native libraries.
• I have taken a further look at how these native libraries were built. Specifically, I looked at the OpenBLAS library. Here is a random compiler command from the built:
  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.o
  Please 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?

• @Peiyang-Song cannot reproduce the issue. This makes me think that they are still working on the machine that built the artifact.
• @Peiyang-Song pointed out that the github workflow (of LeanCopilot) succeeds in its build. But this is no issue of LeanCopilot itself but of the lean4example. Lean4Example does not have a github workflow. I am pretty sure that if it did then the build would fail at least in some cases (it is not clear whether the github hosted runners support AVX-512 -- from what I understand, most of them don't). Why? The build of LeanCopilot actually builds LeanCopilot on the hosted github runner hardware. A build lean4example would make use of the prebuilt binary that only supports some CPUs.
• If I change Lean4Example to use a locally built LeanCopilot artifact, the error goes away.

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]

Thanks for your reply

Hi! I can confirm the behaviour und could track it down further. My explaination goes as follows:

• Lake/Lean make great use of caching and prebuilt binaries. If I have in my lakefile.lean a line like
  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.
• The build log in this case does not actually compile anything in LeanCopilot but rather replay the logs that were gathered during the actual build.
  Actually, this can be seen in the log cited in the first message of @6AlexMan: It contains lines like

/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc: In function

and I'm pretty sure that the home directory of @6AlexMan is not /home/peiyangsong.

• Hence, we can conclude that @Peiyang-Song provided a prebuilt artifact and if others follow the instruction4 for the lean4-example, their build will download that prebuilt artifact.
• Also note that the prebuilt artifact does not only contain LeanCopilot itself but also various native libraries.
• I have taken a further look at how these native libraries were built. Specifically, I looked at the OpenBLAS library. Here is a random compiler command from the built:
  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.o
  Please 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?

• @Peiyang-Song cannot reproduce the issue. This makes me think that they are still working on the machine that built the artifact.
• @Peiyang-Song pointed out that the github workflow (of LeanCopilot) succeeds in its build. But this is no issue of LeanCopilot itself but of the lean4example. Lean4Example does not have a github workflow. I am pretty sure that if it did then the build would fail at least in some cases (it is not clear whether the github hosted runners support AVX-512 -- from what I understand, most of them don't). Why? The build of LeanCopilot actually builds LeanCopilot on the hosted github runner hardware. A build lean4example would make use of the prebuilt binary that only supports some CPUs.
• If I change Lean4Example to use a locally built LeanCopilot artifact, the error goes away.

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.

Thanks for your reply

[Peiyang-Song]

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!