build.sh fails undefined symbol: initialize_Lean_Replay

[robomotic]

Hi there,
I also tried to run the build.sh script from the repository and I get this error:

/home/robomotic/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean: symbol lookup error: 
✖ [527/531] Building LeanCopilot.LlmAesop
.....
././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractProof-1.so: undefined symbol: initialize_Lean_Replay
error: Lean exited with code 127
Some required builds logged failures:
- LeanCopilot.LlmAesop
error: build failed

[robomotic]

I wonder if upgrading this yesterday: https://github.com/lean-dojo/LeanCopilot/blob/main/lean-toolchain to 4.13.0-rc broke the build?

[robomotic]

Reverted now to previous commit 4.11.0 and see if it builds.

[robomotic]

This is more positive as now the errors pertains to missing HF files:

info: ././././LeanCopilotTests/ModelAPIs.lean:5:0: false
info: ././././LeanCopilotTests/ModelAPIs.lean:18:0:
error: ././././LeanCopilotTests/ModelAPIs.lean:18:0: Cannot find the model ct2-leandojo-lean4-tacgen-byt5-small. Please run `lake exe download https://huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small`.
info: ././././LeanCopilotTests/ModelAPIs.lean:26:0:
error: ././././LeanCopilotTests/ModelAPIs.lean:26:0: Cannot find the model ct2-leandojo-lean4-tacgen-byt5-small. Please run `lake exe download https://huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small`.
info: ././././LeanCopilotTests/ModelAPIs.lean:40:0:
error: ././././LeanCopilotTests/ModelAPIs.lean:40:0: Cannot find the model ct2-byt5-small. Please run `lake exe download https://huggingface.co/kaiyuy/ct2-byt5-small`.
info: ././././LeanCopilotTests/ModelAPIs.lean:51:0:
error: ././././LeanCopilotTests/ModelAPIs.lean:51:0: Cannot find the model ct2-leandojo-lean4-retriever-byt5-small. Please run `lake exe download https://huggingface.co/kaiyuy/ct2-leandojo-lean4-retriever-byt5-small`.
info: ././././LeanCopilotTests/ModelAPIs.lean:60:0: #[("Hello, world!", 0.500000), ("Hi!", 0.300000)]
info: ././././LeanCopilotTests/ModelAPIs.lean:69:0: [1.000000, 2.000000, 3.000000]
error: Lean exited with code 1
Some required builds logged failures:
- LeanCopilotTests.PremiseSelection
- LeanCopilotTests.ProofSearch
- LeanCopilotTests.TacticSuggestion
- LeanCopilotTests.ModelAPIs
error: build failed

[krammnic]

Getting same with build.sh

[priamai]

Yes there was a breaking change yesterday, to make it work you should pull the commit: 880f820
With that I was able to build however I get other issues now.

[priamai]

This is where it breaks now:

Some required builds logged failures:
- LeanCopilot/libctranslate2
error: build failed
Updated git hooks.
Git LFS initialized.
ℹ [4/19] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j4`
✖ [5/19] Building LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
error: no such file or directory (error code: 2)
  file: ././.lake/build/lib/libctranslate2.so
Some required builds logged failures:
- LeanCopilot/libctranslate2
error: build failed
ℹ [4/552] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j4`
✖ [5/552] Building LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
error: no such file or directory (error code: 2)
  file: ././.lake/build/lib/libctranslate2.so
Some required builds logged failures:
- LeanCopilot/libctranslate2
error: build failed