Lean Copilot v1.2.2 (standalone, no mathlib) not working

realharryhero commented 1 month ago

When running Lean Copilot v1.2.2 with lean4's language v4.8.0-rc2 (standalone, without mathlib), I receive some warnings and an error. I'm running Ubuntu 22.04. Also, thank you in advance for reading this issue!

lake update LeanCopilot works okay; the output from my running the command is below:

Code

``` 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' ```

lake exe LeanCopilot/download is when issues start popping up:

Code

``` ℹ [3/18] Replayed LeanCopilot/libopenblas info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j8` ℹ [4/18] Replayed LeanCopilot/libctranslate2 info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2 info: Configuring CTranslate2 with `cmake -DBUILD_CLI=OFF -DOPENMP_RUNTIME=NONE -DWITH_DNNL=OFF -DWITH_MKL=OFF -DWITH_ACCELERATE=OFF -DWITH_OPENBLAS=ON -DOPENBLAS_INCLUDE_DIR=../../OpenBLAS -DOPENBLAS_LIBRARY=../../OpenBLAS/libopenblas.so -DWITH_CUDA=OFF -DWITH_CUDNN=OFF ..` info: Building CTranslate2 with `make -j8` info: stdout: [ 1%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/string_view.c.o [ 3%] 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/filesystem.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 [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_arm_linux_or_android.c.o [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_freebsd.c.o [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_mips_linux_or_android.c.o [ 6%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_linux_or_android.c.o [ 7%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_macos.c.o [ 8%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_ppc_linux.c.o [ 9%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_windows.c.o [ 9%] Linking C static library libcpu_features.a [ 9%] Built target cpu_features [ 10%] Building CXX object CMakeFiles/ctranslate2.dir/src/allocator.cc.o [ 11%] Building CXX object CMakeFiles/ctranslate2.dir/src/buffered_translation_wrapper.cc.o [ 13%] Building CXX object CMakeFiles/ctranslate2.dir/src/batch_reader.cc.o [ 14%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/allocator.cc.o [ 14%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/backend.cc.o [ 15%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/cpu_info.cc.o [ 16%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/kernels.cc.o [ 17%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/cpu_isa.cc.o [ 17%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/parallel.cc.o [ 18%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/primitives.cc.o [ 19%] Building CXX object CMakeFiles/ctranslate2.dir/src/decoding_utils.cc.o [ 20%] Building CXX object CMakeFiles/ctranslate2.dir/src/decoding.cc.o [ 20%] Building CXX object CMakeFiles/ctranslate2.dir/src/devices.cc.o [ 21%] Building CXX object CMakeFiles/ctranslate2.dir/src/dtw.cc.o [ 22%] Building CXX object CMakeFiles/ctranslate2.dir/src/encoder.cc.o [ 23%] Building CXX object CMakeFiles/ctranslate2.dir/src/env.cc.o [ 25%] Building CXX object CMakeFiles/ctranslate2.dir/src/filesystem.cc.o [ 25%] Building CXX object CMakeFiles/ctranslate2.dir/src/generator.cc.o [ 26%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/attention_layer.cc.o [ 27%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/attention.cc.o [ 28%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/flash_attention.cc.o [ 28%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/common.cc.o [ 29%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/decoder.cc.o [ 30%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/transformer.cc.o [ 31%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/wav2vec2.cc.o [ 31%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/whisper.cc.o [ 32%] Building CXX object CMakeFiles/ctranslate2.dir/src/logging.cc.o [ 33%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/language_model.cc.o [ 34%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model.cc.o [ 35%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model_factory.cc.o [ 35%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model_reader.cc.o [ 36%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/sequence_to_sequence.cc.o [ 38%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/transformer.cc.o [ 39%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/wav2vec2.cc.o [ 39%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/whisper.cc.o [ 40%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/activation.cc.o [ 41%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/add.cc.o [ 42%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/alibi_add.cc.o [ 42%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/alibi_add_cpu.cc.o [ 43%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/bias_add.cc.o [ 44%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/bias_add_cpu.cc.o [ 45%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/concat.cc.o [ 46%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/concat_split_slide_cpu.cc.o [ 46%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/conv1d.cc.o [ 47%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/conv1d_cpu.cc.o [ 48%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/cos.cc.o [ 50%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/dequantize.cc.o [ 50%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/dequantize_cpu.cc.o [ 51%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/flash_attention.cc.o [ 52%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/flash_attention_cpu.cc.o [ 53%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gather.cc.o [ 53%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gather_cpu.cc.o [ 54%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gelu.cc.o [ 55%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gemm.cc.o [ 56%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gumbel_max.cc.o [ 57%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gumbel_max_cpu.cc.o [ 57%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/layer_norm.cc.o [ 58%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/layer_norm_cpu.cc.o [ 59%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/log.cc.o [ 60%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/matmul.cc.o [ 60%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mean.cc.o [ 61%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mean_cpu.cc.o [ 63%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/median_filter.cc.o [ 64%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/min_max.cc.o [ 64%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mul.cc.o [ 65%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/multinomial.cc.o [ 66%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/multinomial_cpu.cc.o [ 67%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/quantize.cc.o [ 68%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/quantize_cpu.cc.o [ 68%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/relu.cc.o [ 69%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rms_norm.cc.o [ 70%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rms_norm_cpu.cc.o [ 71%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rotary.cc.o [ 71%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rotary_cpu.cc.o [ 72%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/sin.cc.o [ 73%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/softmax.cc.o [ 75%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/softmax_cpu.cc.o [ 75%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/split.cc.o [ 76%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/slide.cc.o [ 77%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/sub.cc.o [ 78%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/swish.cc.o [ 79%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tanh.cc.o [ 79%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tile.cc.o [ 80%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tile_cpu.cc.o [ 81%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topk.cc.o [ 82%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topk_cpu.cc.o [ 82%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topp_mask.cc.o [ 83%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topp_mask_cpu.cc.o [ 84%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/transpose.cc.o [ 85%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/nccl_ops.cc.o [ 86%] Building CXX object CMakeFiles/ctranslate2.dir/src/padder.cc.o [ 86%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/nccl_ops_cpu.cc.o [ 88%] Building CXX object CMakeFiles/ctranslate2.dir/src/profiler.cc.o [ 89%] Building CXX object CMakeFiles/ctranslate2.dir/src/random.cc.o [ 90%] Building CXX object CMakeFiles/ctranslate2.dir/src/sampling.cc.o [ 90%] Building CXX object CMakeFiles/ctranslate2.dir/src/scoring.cc.o [ 91%] Building CXX object CMakeFiles/ctranslate2.dir/src/storage_view.cc.o [ 92%] Building CXX object CMakeFiles/ctranslate2.dir/src/thread_pool.cc.o [ 93%] Building CXX object CMakeFiles/ctranslate2.dir/src/translator.cc.o [ 93%] Building CXX object CMakeFiles/ctranslate2.dir/src/types.cc.o [ 94%] Building CXX object CMakeFiles/ctranslate2.dir/src/utils.cc.o [ 95%] Building CXX object CMakeFiles/ctranslate2.dir/src/vocabulary.cc.o [ 96%] Building CXX object CMakeFiles/ctranslate2.dir/src/vocabulary_map.cc.o [ 96%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx.cc.o [ 97%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx2.cc.o [ 98%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx512.cc.o [100%] Linking CXX shared library libctranslate2.so [100%] Built target ctranslate2 info: stderr: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/kernels.cc:19: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc:51:18: warning: unused variable 'is_int8' [-Wunused-variable] const bool is_int8 = (compute_type == ComputeType::INT8 ^ 1 warning generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:43: warning: unused parameter 'transpose_a' [-Wunused-parameter] bool transpose_a, bool transpose_b, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:61: warning: unused parameter 'transpose_b' [-Wunused-parameter] bool transpose_a, bool transpose_b, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:44: warning: unused parameter 'm' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:53: warning: unused parameter 'n' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:62: warning: unused parameter 'k' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:883:44: warning: unused parameter 'alpha' [-Wunused-parameter] float alpha, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:52: warning: unused parameter 'a' [-Wunused-parameter] const int8_t* a, dim_t lda, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:61: warning: unused parameter 'lda' [-Wunused-parameter] const int8_t* a, dim_t lda, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:52: warning: unused parameter 'b' [-Wunused-parameter] const int8_t* b, dim_t ldb, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:61: warning: unused parameter 'ldb' [-Wunused-parameter] const int8_t* b, dim_t ldb, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:886:44: warning: unused parameter 'beta' [-Wunused-parameter] float beta, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:47: warning: unused parameter 'c' [-Wunused-parameter] int32_t* c, dim_t ldc, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:56: warning: unused parameter 'ldc' [-Wunused-parameter] int32_t* c, dim_t ldc, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:888:53: warning: unused parameter 'a_shift_compensation' [-Wunused-parameter] const int32_t* a_shift_compensation) { ^ 1 warning generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:19:65: warning: unused parameter 'values' [-Wunused-parameter] const StorageView& values, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:26:60: warning: unused parameter 'values_padder' [-Wunused-parameter] const Padder* values_padder, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:28:59: warning: unused parameter 'position_bias' [-Wunused-parameter] StorageView* position_bias, ^ 3 warnings generated. 14 warnings generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:448:25: warning: comparison of integers of different signs: 'int' and 'size_t' (aka 'unsigned long') [-Wsign-compare] for (int i = 0; i < num; ++i) { ~ ^ ~~~ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:739:32: warning: comparison of integers of different signs: 'std::vector::size_type' (aka 'unsigned long') and 'int' [-Wsign-compare] if (outputs.size() > current_index && !outputs[current_index].empty()) ~~~~~~~~~~~~~~ ^ ~~~~~~~~~~~~~ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:454:17: warning: unused function 'replace' [-Wunused-function] static bool replace(std::string& str, const std::string& from, const std::string& to) { ^ 3 warnings generated. In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx.cc:13: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx.h:13: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx512.cc:7: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx512.h:6: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx2.cc:10: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx.h:13: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ 1 warning generated. 1 warning generated. 1 warning generated. ℹ [10/18] 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 /home/mfan/.cache/lean_copilot/models/huggingface.co/kaiyuy/ct2-leandojo-lean4-retriever-byt5-small The model is available at /home/mfan/.cache/lean_copilot/models/huggingface.co/kaiyuy/ct2-byt5-small The model is available at /home/mfan/.cache/lean_copilot/models/huggingface.co/kaiyuy/premise-embeddings-leandojo-lean4-retriever-byt5-small The model is available at /home/mfan/.cache/lean_copilot/models/huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small Done! ```

lake build also has some issues:

Code

``` ℹ [3/14] Replayed LeanCopilot/libopenblas info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j8` ℹ [6/14] Replayed LeanCopilot/libctranslate2 info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2 info: Configuring CTranslate2 with `cmake -DBUILD_CLI=OFF -DOPENMP_RUNTIME=NONE -DWITH_DNNL=OFF -DWITH_MKL=OFF -DWITH_ACCELERATE=OFF -DWITH_OPENBLAS=ON -DOPENBLAS_INCLUDE_DIR=../../OpenBLAS -DOPENBLAS_LIBRARY=../../OpenBLAS/libopenblas.so -DWITH_CUDA=OFF -DWITH_CUDNN=OFF ..` info: Building CTranslate2 with `make -j8` info: stdout: [ 1%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/string_view.c.o [ 3%] 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/filesystem.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 [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_arm_linux_or_android.c.o [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_freebsd.c.o [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_mips_linux_or_android.c.o [ 6%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_linux_or_android.c.o [ 7%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_macos.c.o [ 8%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_ppc_linux.c.o [ 9%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_windows.c.o [ 9%] Linking C static library libcpu_features.a [ 9%] Built target cpu_features [ 10%] Building CXX object CMakeFiles/ctranslate2.dir/src/allocator.cc.o [ 11%] Building CXX object CMakeFiles/ctranslate2.dir/src/buffered_translation_wrapper.cc.o [ 13%] Building CXX object CMakeFiles/ctranslate2.dir/src/batch_reader.cc.o [ 14%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/allocator.cc.o [ 14%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/backend.cc.o [ 15%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/cpu_info.cc.o [ 16%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/kernels.cc.o [ 17%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/cpu_isa.cc.o [ 17%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/parallel.cc.o [ 18%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/primitives.cc.o [ 19%] Building CXX object CMakeFiles/ctranslate2.dir/src/decoding_utils.cc.o [ 20%] Building CXX object CMakeFiles/ctranslate2.dir/src/decoding.cc.o [ 20%] Building CXX object CMakeFiles/ctranslate2.dir/src/devices.cc.o [ 21%] Building CXX object CMakeFiles/ctranslate2.dir/src/dtw.cc.o [ 22%] Building CXX object CMakeFiles/ctranslate2.dir/src/encoder.cc.o [ 23%] Building CXX object CMakeFiles/ctranslate2.dir/src/env.cc.o [ 25%] Building CXX object CMakeFiles/ctranslate2.dir/src/filesystem.cc.o [ 25%] Building CXX object CMakeFiles/ctranslate2.dir/src/generator.cc.o [ 26%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/attention_layer.cc.o [ 27%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/attention.cc.o [ 28%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/flash_attention.cc.o [ 28%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/common.cc.o [ 29%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/decoder.cc.o [ 30%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/transformer.cc.o [ 31%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/wav2vec2.cc.o [ 31%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/whisper.cc.o [ 32%] Building CXX object CMakeFiles/ctranslate2.dir/src/logging.cc.o [ 33%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/language_model.cc.o [ 34%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model.cc.o [ 35%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model_factory.cc.o [ 35%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model_reader.cc.o [ 36%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/sequence_to_sequence.cc.o [ 38%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/transformer.cc.o [ 39%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/wav2vec2.cc.o [ 39%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/whisper.cc.o [ 40%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/activation.cc.o [ 41%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/add.cc.o [ 42%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/alibi_add.cc.o [ 42%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/alibi_add_cpu.cc.o [ 43%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/bias_add.cc.o [ 44%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/bias_add_cpu.cc.o [ 45%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/concat.cc.o [ 46%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/concat_split_slide_cpu.cc.o [ 46%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/conv1d.cc.o [ 47%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/conv1d_cpu.cc.o [ 48%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/cos.cc.o [ 50%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/dequantize.cc.o [ 50%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/dequantize_cpu.cc.o [ 51%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/flash_attention.cc.o [ 52%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/flash_attention_cpu.cc.o [ 53%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gather.cc.o [ 53%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gather_cpu.cc.o [ 54%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gelu.cc.o [ 55%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gemm.cc.o [ 56%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gumbel_max.cc.o [ 57%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gumbel_max_cpu.cc.o [ 57%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/layer_norm.cc.o [ 58%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/layer_norm_cpu.cc.o [ 59%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/log.cc.o [ 60%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/matmul.cc.o [ 60%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mean.cc.o [ 61%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mean_cpu.cc.o [ 63%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/median_filter.cc.o [ 64%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/min_max.cc.o [ 64%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mul.cc.o [ 65%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/multinomial.cc.o [ 66%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/multinomial_cpu.cc.o [ 67%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/quantize.cc.o [ 68%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/quantize_cpu.cc.o [ 68%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/relu.cc.o [ 69%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rms_norm.cc.o [ 70%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rms_norm_cpu.cc.o [ 71%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rotary.cc.o [ 71%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rotary_cpu.cc.o [ 72%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/sin.cc.o [ 73%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/softmax.cc.o [ 75%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/softmax_cpu.cc.o [ 75%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/split.cc.o [ 76%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/slide.cc.o [ 77%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/sub.cc.o [ 78%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/swish.cc.o [ 79%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tanh.cc.o [ 79%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tile.cc.o [ 80%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tile_cpu.cc.o [ 81%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topk.cc.o [ 82%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topk_cpu.cc.o [ 82%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topp_mask.cc.o [ 83%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topp_mask_cpu.cc.o [ 84%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/transpose.cc.o [ 85%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/nccl_ops.cc.o [ 86%] Building CXX object CMakeFiles/ctranslate2.dir/src/padder.cc.o [ 86%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/nccl_ops_cpu.cc.o [ 88%] Building CXX object CMakeFiles/ctranslate2.dir/src/profiler.cc.o [ 89%] Building CXX object CMakeFiles/ctranslate2.dir/src/random.cc.o [ 90%] Building CXX object CMakeFiles/ctranslate2.dir/src/sampling.cc.o [ 90%] Building CXX object CMakeFiles/ctranslate2.dir/src/scoring.cc.o [ 91%] Building CXX object CMakeFiles/ctranslate2.dir/src/storage_view.cc.o [ 92%] Building CXX object CMakeFiles/ctranslate2.dir/src/thread_pool.cc.o [ 93%] Building CXX object CMakeFiles/ctranslate2.dir/src/translator.cc.o [ 93%] Building CXX object CMakeFiles/ctranslate2.dir/src/types.cc.o [ 94%] Building CXX object CMakeFiles/ctranslate2.dir/src/utils.cc.o [ 95%] Building CXX object CMakeFiles/ctranslate2.dir/src/vocabulary.cc.o [ 96%] Building CXX object CMakeFiles/ctranslate2.dir/src/vocabulary_map.cc.o [ 96%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx.cc.o [ 97%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx2.cc.o [ 98%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx512.cc.o [100%] Linking CXX shared library libctranslate2.so [100%] Built target ctranslate2 info: stderr: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/kernels.cc:19: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc:51:18: warning: unused variable 'is_int8' [-Wunused-variable] const bool is_int8 = (compute_type == ComputeType::INT8 ^ 1 warning generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:43: warning: unused parameter 'transpose_a' [-Wunused-parameter] bool transpose_a, bool transpose_b, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:61: warning: unused parameter 'transpose_b' [-Wunused-parameter] bool transpose_a, bool transpose_b, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:44: warning: unused parameter 'm' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:53: warning: unused parameter 'n' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:62: warning: unused parameter 'k' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:883:44: warning: unused parameter 'alpha' [-Wunused-parameter] float alpha, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:52: warning: unused parameter 'a' [-Wunused-parameter] const int8_t* a, dim_t lda, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:61: warning: unused parameter 'lda' [-Wunused-parameter] const int8_t* a, dim_t lda, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:52: warning: unused parameter 'b' [-Wunused-parameter] const int8_t* b, dim_t ldb, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:61: warning: unused parameter 'ldb' [-Wunused-parameter] const int8_t* b, dim_t ldb, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:886:44: warning: unused parameter 'beta' [-Wunused-parameter] float beta, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:47: warning: unused parameter 'c' [-Wunused-parameter] int32_t* c, dim_t ldc, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:56: warning: unused parameter 'ldc' [-Wunused-parameter] int32_t* c, dim_t ldc, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:888:53: warning: unused parameter 'a_shift_compensation' [-Wunused-parameter] const int32_t* a_shift_compensation) { ^ 1 warning generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:19:65: warning: unused parameter 'values' [-Wunused-parameter] const StorageView& values, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:26:60: warning: unused parameter 'values_padder' [-Wunused-parameter] const Padder* values_padder, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:28:59: warning: unused parameter 'position_bias' [-Wunused-parameter] StorageView* position_bias, ^ 3 warnings generated. 14 warnings generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:448:25: warning: comparison of integers of different signs: 'int' and 'size_t' (aka 'unsigned long') [-Wsign-compare] for (int i = 0; i < num; ++i) { ~ ^ ~~~ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:739:32: warning: comparison of integers of different signs: 'std::vector::size_type' (aka 'unsigned long') and 'int' [-Wsign-compare] if (outputs.size() > current_index && !outputs[current_index].empty()) ~~~~~~~~~~~~~~ ^ ~~~~~~~~~~~~~ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:454:17: warning: unused function 'replace' [-Wunused-function] static bool replace(std::string& str, const std::string& from, const std::string& to) { ^ 3 warnings generated. In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx.cc:13: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx.h:13: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx512.cc:7: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx512.h:6: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx2.cc:10: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx.h:13: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ 1 warning generated. 1 warning generated. 1 warning generated. Build completed successfully. ```

Finally, importing LeanCopilot works okay, but then trying to use suggest_tactics causes lean4 to crash, shown below: (reduced quality to save space)

https://github.com/lean-dojo/LeanCopilot/assets/118628756/de5999fa-a833-46fa-b462-1349d9ca20cd

I've also run:

Lean Copilot v1.2.1 with lean4's language v4.8.0-rc1 with mathlib4's version v4.8.0-rc1, which didn't work (similar issues occurred here; quite similar, actually, implying perhaps that v1.2.1 onwards may not be working too correctly. I don't believe there were much issues in mathlib4 (maybe there were), so maybe the fix for v1.2.1 previously may have caused a few issues.
Lean Copilot v1.2.0 with lean4's language v4.7.0 with mathlib4's version v4.7.0 (copied from my repo), which did work for a bit (probably it stopped working after some time because the mathlib directory probably refers to some other code that does tests with the original repo that I copied from and/or uses the original repo in some other way).

Thank you for replying in advance!

Peiyang-Song commented 1 month ago

Hi @realharryhero , thanks for the detailed report! I just tried Lean Copilot v1.2.2 again with my Ubuntu machine, but wasn't able to reproduce the error in your screenshot. From reading your code, it seems to me that all the messages during downloading and building are just warnings instead of errors. Is it true that an explicit error message did not ever appear during your entire experience? (Other than the server crash which, I suspect, didn't give much meaningful information.)

realharryhero commented 1 month ago

Yes, that's true (it could be something wrong on my end then). When my server crashed, there was some information in the "Output" tab of the terminal of VSCode, shown below:

Code

``` [Error - 11:31:19 PM] Request textDocument/foldingRange failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/codeAction failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/documentSymbol failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/semanticTokens/range failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/codeAction failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/codeAction failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/documentSymbol failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:19 PM] Request textDocument/codeAction failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:27 PM] Request textDocument/codeAction failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 [Error - 11:31:35 PM] Request textDocument/codeAction failed. Message: Server process for file:///home/mfan/leanproject3/Main.lean crashed, likely due to a stack overflow or a bug. Code: -32902 ```

I'll check if anything is wrong with my lean4 installation by uninstalling and reinstalling lean4, turning on and off the LEAN extension, etc. Thank you!

efessas commented 1 month ago

Hi, @realharryhero have you solved the issue? I am also having some problem running lean 4.8.0-rc2, but my problem may be different, here is the error info(when running lake exe LeanCopilot/download command) :


ℹ [3/18] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j8`
✖ [4/18] Building LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
error: no such file or directory (error code: 2)
  file: ././.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.so
Some builds logged failures:
- LeanCopilot/libctranslate2
error: build failed

there is a file named libctranslate2.so.log.json in the directory of that missing file reported. if I rename that file (sorry I am not sure if this is the right way) then here is the error info:


ℹ [3/18] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j8`
✖ [4/18] Replaying LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
trace: ././.lake/packages/LeanCopilot/.lake/build> git clone --recursive https://github.com/OpenNMT/CTranslate2
trace: stderr:
fatal: destination path 'CTranslate2' already exists and is not an empty directory.
error: external command 'git' exited with code 128
✖ [5/18] Building LeanCopilot/ct2.o
trace: .> c++ -c -o ././.lake/packages/LeanCopilot/.lake/build/cpp/ct2.o ././.lake/packages/LeanCopilot/cpp/ct2.cpp -fPIC -std=c++17 -O3 -I /home/efessas/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/include -I ././.lake/packages/LeanCopilot/.lake/build/include
info: stderr:
././.lake/packages/LeanCopilot/cpp/ct2.cpp:1:10: fatal error: ctranslate2/devices.h: No such file or directory
    1 | #include <ctranslate2/devices.h>
      |          ^~~~~~~~~~~~~~~~~~~~~~~
compilation terminated.
error: external command 'c++' exited with code 1
Some builds logged failures:
- LeanCopilot/libctranslate2
- LeanCopilot/ct2.o
error: build failed

Again, very appreciate for @Peiyang-Song 's hard work!

Btw, when I try 4.8.0-rc1 several days before, the similiar warning occur as @realharryhero reported, and importing LeanCopilot in lean just failed.

edit: I have mathlib imported

Peiyang-Song commented 1 month ago

Hi @efessas , thank you for the error report! It seems to me that what you are encountering may be different from @realharryhero , since your log contains explicit errors indicating a building failure. I will try to reproduce your errors when I get a chance. Could you include your OS information and whether you are on a CUDA-enabled GPU or just CPU?

efessas commented 1 month ago

Hi @Peiyang-Song, I am running on Ubuntu 22.04, and my PC has a RTX3060 GPU with CUDA 11.5.

realharryhero commented 1 month ago

(Only read this post after the second post; i.e. read this post if you have time)

(Though I checked around 2, 3 days ago only, I believe, and didn't post for a while for a reason explained later) It doesn't seem that there are any errors with my LEAN installation:

I can run LEAN alright. I do need "lake env" before I run code (that is, "lean --run $FILE" doesn't work, as "lake env lean --run $FILE" does; I think this is normal for many people as well, though - check this stack exchange link.)
mathlib4 works on my computer.
I do essentially no dumb stuff on my computer, so there isn't any large thing taking up space; it's mainly just a Ubuntu computer.

Other minor details that may not have much to do with the installation:

- Regarding the third bullet point, though, I believe the Ubuntu computer / its CPUs in some ways were "minimally installed," so a few packages were removed (that is, for example cpufreq does not exist on my computer). But I don't think this has much to do with the LEAN installation. - I am SSH-ing onto my computer with the VS Code Remote extensions, but I don't think this would cause an issue as I've run other packages before.

It's moreover confusing to figure out where precisely to look for where the LEAN installation's having issues.

I didn't post for a while because I wanted to check if I could run LeanCopilot with my Mac, which I've been trying to do but one package (brew) can only install for specific kinds of Macs, and it's almost working. I'll post those results shortly if I happen to get that installation working.

Maybe to whoever (could be anyone) is reading this issue currently - could whomever install LeanCopilot with a different computer, and see if the results could be replicated? Perhaps if there's an issue with LeanCopilot on the other computer, then it could be because the current computer has something else installed (that isn't installed on all normal installations) that allows LeanCopilot to work. Thank you!

realharryhero commented 1 month ago

Please disregard the post above; I do have tangible error information:

https://github.com/lean-dojo/LeanCopilot/assets/118628756/99e551c7-a37f-4d5c-a54c-05d14a80c01c

Explaining the video:

First, before the video, I installed all parts of the code, following the manual. (No errors occurred here.)
Then I imported LeanCopilot on a file by writing "import LeanCopilot", from which a loading bar started; the first few seconds of the video showed the loading bar completing.
Then I went through all the steps of the installation again. lake update LeanCopilot worked okay; lake exe LeanCopilot/download worked fine as well; but lake build had some errors.

The error information is below:

My section header in bold

ℹ [5/499] Replayed LeanCopilot/libopenblas info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j8` ℹ [6/499] Replayed LeanCopilot/libctranslate2 info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2 info: Configuring CTranslate2 with `cmake -DBUILD_CLI=OFF -DOPENMP_RUNTIME=NONE -DWITH_DNNL=OFF -DWITH_MKL=OFF -DWITH_ACCELERATE=OFF -DWITH_OPENBLAS=ON -DOPENBLAS_INCLUDE_DIR=../../OpenBLAS -DOPENBLAS_LIBRARY=../../OpenBLAS/libopenblas.so -DWITH_CUDA=OFF -DWITH_CUDNN=OFF ..` info: Building CTranslate2 with `make -j8` info: stdout: [ 1%] Building C object third_party/cpu_features/CMakeFiles/utils.dir/src/string_view.c.o [ 3%] 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/filesystem.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 [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_arm_linux_or_android.c.o [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_freebsd.c.o [ 5%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_mips_linux_or_android.c.o [ 6%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_linux_or_android.c.o [ 7%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_macos.c.o [ 8%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_ppc_linux.c.o [ 9%] Building C object third_party/cpu_features/CMakeFiles/cpu_features.dir/src/impl_x86_windows.c.o [ 9%] Linking C static library libcpu_features.a [ 9%] Built target cpu_features [ 10%] Building CXX object CMakeFiles/ctranslate2.dir/src/allocator.cc.o [ 11%] Building CXX object CMakeFiles/ctranslate2.dir/src/buffered_translation_wrapper.cc.o [ 13%] Building CXX object CMakeFiles/ctranslate2.dir/src/batch_reader.cc.o [ 14%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/allocator.cc.o [ 14%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/backend.cc.o [ 15%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/cpu_info.cc.o [ 16%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/kernels.cc.o [ 17%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/cpu_isa.cc.o [ 17%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/parallel.cc.o [ 18%] Building CXX object CMakeFiles/ctranslate2.dir/src/cpu/primitives.cc.o [ 19%] Building CXX object CMakeFiles/ctranslate2.dir/src/decoding_utils.cc.o [ 20%] Building CXX object CMakeFiles/ctranslate2.dir/src/decoding.cc.o [ 20%] Building CXX object CMakeFiles/ctranslate2.dir/src/devices.cc.o [ 21%] Building CXX object CMakeFiles/ctranslate2.dir/src/dtw.cc.o [ 22%] Building CXX object CMakeFiles/ctranslate2.dir/src/encoder.cc.o [ 23%] Building CXX object CMakeFiles/ctranslate2.dir/src/env.cc.o [ 25%] Building CXX object CMakeFiles/ctranslate2.dir/src/filesystem.cc.o [ 25%] Building CXX object CMakeFiles/ctranslate2.dir/src/generator.cc.o [ 26%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/attention_layer.cc.o [ 27%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/attention.cc.o [ 28%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/flash_attention.cc.o [ 28%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/common.cc.o [ 29%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/decoder.cc.o [ 30%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/transformer.cc.o [ 31%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/wav2vec2.cc.o [ 31%] Building CXX object CMakeFiles/ctranslate2.dir/src/layers/whisper.cc.o [ 32%] Building CXX object CMakeFiles/ctranslate2.dir/src/logging.cc.o [ 33%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/language_model.cc.o [ 34%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model.cc.o [ 35%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model_factory.cc.o [ 35%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/model_reader.cc.o [ 36%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/sequence_to_sequence.cc.o [ 38%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/transformer.cc.o [ 39%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/wav2vec2.cc.o [ 39%] Building CXX object CMakeFiles/ctranslate2.dir/src/models/whisper.cc.o [ 40%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/activation.cc.o [ 41%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/add.cc.o [ 42%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/alibi_add.cc.o [ 42%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/alibi_add_cpu.cc.o [ 43%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/bias_add.cc.o [ 44%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/bias_add_cpu.cc.o [ 45%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/concat.cc.o [ 46%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/concat_split_slide_cpu.cc.o [ 46%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/conv1d.cc.o [ 47%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/conv1d_cpu.cc.o [ 48%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/cos.cc.o [ 50%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/dequantize.cc.o [ 50%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/dequantize_cpu.cc.o [ 51%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/flash_attention.cc.o [ 52%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/flash_attention_cpu.cc.o [ 53%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gather.cc.o [ 53%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gather_cpu.cc.o [ 54%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gelu.cc.o [ 55%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gemm.cc.o [ 56%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gumbel_max.cc.o [ 57%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/gumbel_max_cpu.cc.o [ 57%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/layer_norm.cc.o [ 58%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/layer_norm_cpu.cc.o [ 59%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/log.cc.o [ 60%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/matmul.cc.o [ 60%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mean.cc.o [ 61%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mean_cpu.cc.o [ 63%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/median_filter.cc.o [ 64%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/min_max.cc.o [ 64%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/mul.cc.o [ 65%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/multinomial.cc.o [ 66%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/multinomial_cpu.cc.o [ 67%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/quantize.cc.o [ 68%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/quantize_cpu.cc.o [ 68%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/relu.cc.o [ 69%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rms_norm.cc.o [ 70%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rms_norm_cpu.cc.o [ 71%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rotary.cc.o [ 71%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/rotary_cpu.cc.o [ 72%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/sin.cc.o [ 73%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/softmax.cc.o [ 75%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/softmax_cpu.cc.o [ 75%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/split.cc.o [ 76%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/slide.cc.o [ 77%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/sub.cc.o [ 78%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/swish.cc.o [ 79%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tanh.cc.o [ 79%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tile.cc.o [ 80%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/tile_cpu.cc.o [ 81%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topk.cc.o [ 82%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topk_cpu.cc.o [ 82%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topp_mask.cc.o [ 83%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/topp_mask_cpu.cc.o [ 84%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/transpose.cc.o [ 85%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/nccl_ops.cc.o [ 86%] Building CXX object CMakeFiles/ctranslate2.dir/src/padder.cc.o [ 86%] Building CXX object CMakeFiles/ctranslate2.dir/src/ops/nccl_ops_cpu.cc.o [ 88%] Building CXX object CMakeFiles/ctranslate2.dir/src/profiler.cc.o [ 89%] Building CXX object CMakeFiles/ctranslate2.dir/src/random.cc.o [ 90%] Building CXX object CMakeFiles/ctranslate2.dir/src/sampling.cc.o [ 90%] Building CXX object CMakeFiles/ctranslate2.dir/src/scoring.cc.o [ 91%] Building CXX object CMakeFiles/ctranslate2.dir/src/storage_view.cc.o [ 92%] Building CXX object CMakeFiles/ctranslate2.dir/src/thread_pool.cc.o [ 93%] Building CXX object CMakeFiles/ctranslate2.dir/src/translator.cc.o [ 93%] Building CXX object CMakeFiles/ctranslate2.dir/src/types.cc.o [ 94%] Building CXX object CMakeFiles/ctranslate2.dir/src/utils.cc.o [ 95%] Building CXX object CMakeFiles/ctranslate2.dir/src/vocabulary.cc.o [ 96%] Building CXX object CMakeFiles/ctranslate2.dir/src/vocabulary_map.cc.o [ 96%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx.cc.o [ 97%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx2.cc.o [ 98%] Building CXX object CMakeFiles/ctranslate2.dir/kernels_avx512.cc.o [100%] Linking CXX shared library libctranslate2.so [100%] Built target ctranslate2 info: stderr: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/kernels.cc:19: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/backend.cc:51:18: warning: unused variable 'is_int8' [-Wunused-variable] const bool is_int8 = (compute_type == ComputeType::INT8 ^ 1 warning generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:43: warning: unused parameter 'transpose_a' [-Wunused-parameter] bool transpose_a, bool transpose_b, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:881:61: warning: unused parameter 'transpose_b' [-Wunused-parameter] bool transpose_a, bool transpose_b, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:44: warning: unused parameter 'm' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:53: warning: unused parameter 'n' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:882:62: warning: unused parameter 'k' [-Wunused-parameter] dim_t m, dim_t n, dim_t k, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:883:44: warning: unused parameter 'alpha' [-Wunused-parameter] float alpha, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:52: warning: unused parameter 'a' [-Wunused-parameter] const int8_t* a, dim_t lda, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:884:61: warning: unused parameter 'lda' [-Wunused-parameter] const int8_t* a, dim_t lda, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:52: warning: unused parameter 'b' [-Wunused-parameter] const int8_t* b, dim_t ldb, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:885:61: warning: unused parameter 'ldb' [-Wunused-parameter] const int8_t* b, dim_t ldb, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:886:44: warning: unused parameter 'beta' [-Wunused-parameter] float beta, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:47: warning: unused parameter 'c' [-Wunused-parameter] int32_t* c, dim_t ldc, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:887:56: warning: unused parameter 'ldc' [-Wunused-parameter] int32_t* c, dim_t ldc, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/primitives.cc:888:53: warning: unused parameter 'a_shift_compensation' [-Wunused-parameter] const int32_t* a_shift_compensation) { ^ 1 warning generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:19:65: warning: unused parameter 'values' [-Wunused-parameter] const StorageView& values, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:26:60: warning: unused parameter 'values_padder' [-Wunused-parameter] const Padder* values_padder, ^ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/layers/flash_attention.cc:28:59: warning: unused parameter 'position_bias' [-Wunused-parameter] StorageView* position_bias, ^ 3 warnings generated. 14 warnings generated. /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:448:25: warning: comparison of integers of different signs: 'int' and 'size_t' (aka 'unsigned long') [-Wsign-compare] for (int i = 0; i < num; ++i) { ~ ^ ~~~ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:739:32: warning: comparison of integers of different signs: 'std::vector::size_type' (aka 'unsigned long') and 'int' [-Wsign-compare] if (outputs.size() > current_index && !outputs[current_index].empty()) ~~~~~~~~~~~~~~ ^ ~~~~~~~~~~~~~ /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:454:17: warning: unused function 'replace' [-Wunused-function] static bool replace(std::string& str, const std::string& from, const std::string& to) { ^ 3 warnings generated. In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx.cc:13: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx.h:13: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx512.cc:7: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx512.h:6: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/build/kernels_avx2.cc:10: In file included from /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec_avx.h:13: /home/ubuntu/LeanCopilot/.lake/build/CTranslate2/src/cpu/vec.h:148:65: warning: unused parameter 'count' [-Wunused-parameter] static inline void convert_and_store(float v, U* a, dim_t count) { ^ 1 warning generated. 1 warning generated. 1 warning generated. ℹ [12/499] 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" ✖ [499/499] Building leanproject5 trace: .> /home/mfan/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/leanc -o ././.lake/build/bin/leanproject5 ././.lake/build/ir/Main.c.o.export ././.lake/build/ir/Leanproject5/Basic.c.o.export ././.lake/build/ir/Leanproject5.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/ModelCheckpointManager/Url.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/ModelCheckpointManager/Download.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/ModelCheckpointManager.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/Native.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/ByT5.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/Builtin.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/Interface.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/External.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/Generic.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/FFI.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Init/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/CodeAction/Attr.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/CodeAction/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Position.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/CodeAction/Deprecated.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Alias.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/AssocList.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Classes/SatisfiesM.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Monadic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Classes/BEq.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/HashMap/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Control/ForInStep/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Control/ForInStep/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Init.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/List/Init/Attach.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Init/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/SeqFocus.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Util/ProofWanted.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/HashMap/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Nat/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/HashMap/WF.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/HashMap.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models/Registry.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Models.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Options.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/MLList/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Lint/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Lint/Misc.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Control/Nondet/Basic.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Frontend.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Nanos.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Util/UnionFind.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Merge.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Util/UnorderedArraySet.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Classes/Order.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/UInt.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/Char.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Lemmas.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/String.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Expr.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/Expr.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/PersistentHashMap.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/DiscrTree.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/PersistentHashSet.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Util/Basic.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Tactics.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Check.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Rule/Name.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tracing.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RulePattern.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Index/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Options/Public.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Options/Internal.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Options.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Percent.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Util/Tactic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/MonadBacktrack.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/SavedState.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Util/EqualUpToIds.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/Clear.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/Inaccessible.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/HashSet.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/PermuteGoals.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Script.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Rule/Basic.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/InstantiateMVars.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Index.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Rule.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleSet/Member.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleSet/Name.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleSet/Filter.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleSet.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/Extension/Init.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/Extension.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/ElabM.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/ElabRuleTerm.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Apply.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/Cases.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Cases.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Constructors.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/NormSimp.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Tactic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Default.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Forward.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder/Unfold.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Builder.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/RuleExpr.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/Attribute.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/Apply.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/UnusedNames.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Lean/Meta/AssertHypotheses.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/Forward.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/Preprocess.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac/Tactic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/RuleTac.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Expansion/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Expansion/Simp.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Constants.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/UnsafeQueue.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/Data.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/Traversal.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/RunMetaM.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/TreeM.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/AddRapp.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/State.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/Check.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/Tracing.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/ExtractProof.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/ExtractScript.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree/Free.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Tree.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Queue/Class.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Stats/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/SearchM.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/RuleSelection.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Expansion/Norm.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Expansion.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Exception.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/ExpandSafePrefix.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Data/BinomialHeap/Basic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Queue.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Search/Main.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/Assumption.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/ApplyHyps.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/DestructProducts.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/Ext.c.o.export ././.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/OpenPrivate.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/Intros.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/Split.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules/Subst.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Stats/Extension.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Stats/Report.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/Command.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend/Tactic.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Frontend.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/BuiltinRules.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop/Main.c.o.export ././.lake/packages/aesop/.lake/build/ir/Aesop.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/LlmAesop.c.o.export ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot.c.o.export ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a -L./.lake/packages/LeanCopilot/.lake/build/lib -lctranslate2 info: stderr: ld.lld: error: undefined symbol: std::__cxx11::basic_string, std::allocator>::_M_create(unsigned long&, unsigned long) >>> referenced by ct2.cpp >>> ct2.o:(is_generator_initialized) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(is_encoder_initialized) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 48 more times ld.lld: error: undefined symbol: std::__throw_bad_array_new_length() >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(encode) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 18 more times ld.lld: error: undefined symbol: std::runtime_error::runtime_error(std::__cxx11::basic_string, std::allocator> const&) >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(encode) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(bool init_model(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 2 more times ld.lld: error: undefined symbol: std::invalid_argument::invalid_argument(char const*) >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(generate) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 2 more times ld.lld: error: undefined symbol: __libc_single_threaded >>> referenced by ct2.cpp >>> ct2.o:(encode) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(std::future::get()) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(std::__basic_future::~__basic_future()) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 7 more times ld.lld: error: undefined symbol: std::basic_ifstream>::basic_ifstream(char const*, std::_Ios_Openmode) >>> referenced by ct2.cpp >>> ct2.o:(init_premise_embeddings) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(bool init_model(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 1 more times ld.lld: error: undefined symbol: VTT for std::basic_ifstream> >>> referenced by ct2.cpp >>> ct2.o:(init_premise_embeddings) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(bool init_model(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 2 more times ld.lld: error: undefined symbol: std::basic_filebuf>::~basic_filebuf() >>> referenced by ct2.cpp >>> ct2.o:(init_premise_embeddings) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 3 more times ld.lld: error: undefined symbol: std::ios_base::~ios_base() >>> referenced by ct2.cpp >>> ct2.o:(init_premise_embeddings) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 4 more times ld.lld: error: undefined symbol: std::basic_ifstream>::basic_ifstream(std::__cxx11::basic_string, std::allocator> const&, std::_Ios_Openmode) >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(npy::npy_data npy::read_npy(std::__cxx11::basic_string, std::allocator> const&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a ld.lld: error: undefined symbol: std::basic_ifstream>::~basic_ifstream() >>> referenced by ct2.cpp >>> ct2.o:(init_premise_dictionary) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(npy::npy_data npy::read_npy(std::__cxx11::basic_string, std::allocator> const&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a ld.lld: error: undefined symbol: std::__cxx11::basic_string, std::allocator>::_M_construct(unsigned long, char) >>> referenced by ct2.cpp >>> ct2.o:(retrieve) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(retrieve) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(retrieve) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 6 more times ld.lld: error: undefined symbol: std::__throw_length_error(char const*) >>> referenced by ct2.cpp >>> ct2.o:(retrieve) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(bool init_model(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(bool init_model(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 52 more times ld.lld: error: undefined symbol: std::__throw_logic_error(char const*) >>> referenced by ct2.cpp >>> ct2.o:(std::__cxx11::basic_string, std::allocator>::basic_string>(char const*, std::allocator const&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>& nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>::operator[](char const*)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(std::__cxx11::basic_string, std::allocator>& std::vector, std::allocator>, std::allocator, std::allocator>>>::emplace_back(char const*&&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 1 more times ld.lld: error: undefined symbol: std::__cxx11::basic_string, std::allocator>::_M_append(char const*, unsigned long) >>> referenced by ct2.cpp >>> ct2.o:(std::__cxx11::basic_string, std::allocator> std::operator+, std::allocator>(std::__cxx11::basic_string, std::allocator> const&, char const*)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(std::__cxx11::basic_string, std::allocator> std::operator+, std::allocator>(std::__cxx11::basic_string, std::allocator>&&, std::__cxx11::basic_string, std::allocator>&&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(std::__cxx11::basic_string, std::allocator> std::operator+, std::allocator>(std::__cxx11::basic_string, std::allocator>&&, char const*)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 57 more times ld.lld: error: undefined symbol: std::__throw_out_of_range(char const*) >>> referenced by ct2.cpp >>> ct2.o:(std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>::at(std::__cxx11::basic_string, std::allocator> const&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(std::map, std::allocator>, std::unique_ptr>, std::less, std::allocator>>, std::allocator, std::allocator> const, std::unique_ptr>>>>::at(std::__cxx11::basic_string, std::allocator> const&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(npy::npy_data npy::read_npy(std::istream&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 2 more times ld.lld: error: undefined symbol: std::invalid_argument::invalid_argument(std::__cxx11::basic_string, std::allocator> const&) >>> referenced by ct2.cpp >>> ct2.o:(ctranslate2::StorageView::dim(long) const) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a ld.lld: error: undefined symbol: std::basic_ios>::clear(std::_Ios_Iostate) >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>> nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>::parse>&>(std::basic_ifstream>&, std::function, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>&)>, bool, bool)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>> nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>::parse>&>(std::basic_ifstream>&, std::function, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>&)>, bool, bool)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::detail::parser, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>, nlohmann::json_abi_v3_11_2::detail::input_stream_adapter>::~parser()) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 6 more times ld.lld: error: undefined symbol: std::__cxx11::basic_string, std::allocator>::_M_replace(unsigned long, unsigned long, char const*, unsigned long) >>> referenced by ct2.cpp >>> ct2.o:(std::__cxx11::basic_string, std::allocator> std::operator+, std::allocator>(std::__cxx11::basic_string, std::allocator>&&, std::__cxx11::basic_string, std::allocator>&&)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a ld.lld: error: undefined symbol: std::_Rb_tree_increment(std::_Rb_tree_node_base*) >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>::json_value::destroy(nlohmann::json_abi_v3_11_2::detail::value_t)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::basic_json, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>::json_value::destroy(nlohmann::json_abi_v3_11_2::detail::value_t)) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced by ct2.cpp >>> ct2.o:(nlohmann::json_abi_v3_11_2::detail::json_sax_dom_callback_parser, std::allocator>, bool, long, unsigned long, double, std::allocator, nlohmann::json_abi_v3_11_2::adl_serializer, std::vector>>>::end_object()) in archive ././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.a >>> referenced 2 more times ld.lld: error: too many errors emitted, stopping now (use --error-limit=0 to see all errors) clang: error: linker command failed with exit code 1 (use -v to see invocation) error: external command '/home/mfan/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/leanc' exited with code 1 Some builds logged failures: - leanproject5 error: build failed

Thank you again for reading this!

KunihikoK3 commented 1 month ago

I have a similar error. I'm using WSL ubuntu 24.04 on a Windows laptop with RTX4080. In my case, import LeanCopilot does not work

/home/neil/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/lake setup-file /home/neil/LeanCopilot/LeanCopilotTests/TacticSuggestion.lean Init LeanCopilot --no-build failed:

stderr: ℹ [1/515] Replayed LeanCopilot/libopenblas info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS info: Building OpenBLAS with make NO_LAPACK=1 NO_FORTRAN=1 -j32 ℹ [2/515] Replayed LeanCopilot/libctranslate2 info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2 info: Configuring CTranslate2 with cmake -DBUILD_CLI=OFF -DOPENMP_RUNTIME=NONE -DWITH_DNNL=OFF -DWITH_MKL=OFF -DWITH_ACCELERATE=OFF -DWITH_OPENBLAS=ON -DOPENBLAS_INCLUDE_DIR=../../OpenBLAS -DOPENBLAS_LIBRARY=../../OpenBLAS/libopenblas.so -DWITH_CUDA=OFF -DWITH_CUDNN=OFF .. info: Building CTranslate2 with make -j32 info: stdout:`

realharryhero commented 1 month ago

@Peiyang-Song Could you check my most recent post (it gives very tangible error information)? It also seems to be similar to @KunihikoK3 's issue, as the issue seems to be building lake (shown by the large [1/...] bar). Thank you!

Peiyang-Song commented 1 month ago

Thanks for the detailed information! I'll be able to take a look this coming weekend or early next week.

realharryhero commented 1 month ago

Hello @Peiyang-Song , any updates?

Peiyang-Song commented 1 month ago

Hi @realharryhero , sorry for the delay in reply. I have been pretty sick for the past week or so.

Thanks once again for your detailed report. We have tried Lean Copilot on several different Linux machines with or without a CUDA-enabled GPU, but unfortunately we were unable to replicate the error in your video. So far I am not sure why it fails on your end, but I did see Lean published several new versions. I plan to bump Lean Copilot to the latest Lean version in the coming few days once I recover, and hopefully that may fix the error if it is related to version incompatibility.

realharryhero commented 1 month ago

Alright, thank you; hope you feel better soon!

On the bright side, perhaps there's a way to install Lean Copilot on a previous version of LEAN (v4.7.0).

cd $DIR, where $DIR is a placeholder for the desired repository - so if I wanted $DIR=/home/user, I'd write cd /home/user
git clone --branch v4.7.0 https://github.com/leanprover-community/mathlib4; this creates a new repository $DIR/mathlib4 containing version 4.7.0 of the mathlib4 library.
Make a new LEAN project in $LEANLOC, where $LEANLOC is a placeholder (any desired folder).
Enter into the project.
In $LEANLOC/lakefile.lean, write require mathlib from $DIR/mathlib4.
Restart the LEAN server (you should see a red pop-up on the lower right screen; you can also click that)
In the terminal, write lake update and lake exe cache get.
Restart the LEAN server again.
(Make sure to restart Main.lean if it says to do so, as some imports may be outdated)
Follow the steps in the Lean Copilot installation process to install Lean Copilot v1.2.0 (Importantly, v1.2.0 and not v1.2.2) on the installation.

Here's a recording of me doing steps 1-7 (I can't do 9 as I'm using CUDA 11.8 and CTranslate, a package LeanCopilot uses, requires CUDA 12):

https://github.com/lean-dojo/LeanCopilot/assets/118628756/31f19091-a58d-4d97-afc0-cff37490afce

lean-dojo / LeanCopilot

Lean Copilot v1.2.2 (standalone, no mathlib) not working #75