Docker build fails undefined symbol: initialize_Lean_Replay

[robomotic]

Hello, I am just doing the docker build to avoi dall sort of environment problems:

docker build -t leancopilot:latest -f Dockerfile .

However it fails:

296.3 info: stderr:
296.3 /.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean: symbol lookup error: ././.lake/packages/aesop/.lake/build/lib/libAesop-Tree-ExtractProof-1.so: undefined symbol: initialize_Lean_Replay
296.3 error: Lean exited with code 127
296.3 Some required builds logged failures:
296.3 - LeanCopilot.LlmAesop
296.3 error: build failed
------
Dockerfile:17
--------------------
  15 |     
  16 |     # Build the Lean project.
  17 | >>> RUN lake build
  18 |     RUN lake exe LeanCopilot/download
  19 |     RUN lake build LeanCopilotTests
--------------------
ERROR: failed to solve: process "/bin/sh -c lake build" did not complete successfully: exit code: 1

[robomotic]

Please refer to #128

[krammnic]

Actually there is no normal way to build this and fixes that were discussed in #128 are not actually working

[robomotic]

It does work on my Ubuntu but yes I had to make a few changes.

On Mon, 28 Oct 2024, 11:24 Mark, @.***> wrote:

Actually there is no normal way to build this and fixes that were discussed in #128 https://github.com/lean-dojo/LeanCopilot/issues/128 are not actually working

— Reply to this email directly, view it on GitHub https://github.com/lean-dojo/LeanCopilot/issues/127#issuecomment-2441313381, or unsubscribe https://github.com/notifications/unsubscribe-auth/AACNEPG3KA7KGR7WYKFVQ2TZ5YNFJAVCNFSM6AAAAABQHPROUOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINBRGMYTGMZYGE . You are receiving this because you authored the thread.Message ID: @.***>

[krammnic]

It does work on my Ubuntu but yes I had to make a few changes. … On Mon, 28 Oct 2024, 11:24 Mark, @.> wrote: Actually there is no normal way to build this and fixes that were discussed in #128 <#128> are not actually working — Reply to this email directly, view it on GitHub <#127 (comment)>, or unsubscribe https://github.com/notifications/unsubscribe-auth/AACNEPG3KA7KGR7WYKFVQ2TZ5YNFJAVCNFSM6AAAAABQHPROUOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINBRGMYTGMZYGE . You are receiving this because you authored the thread.Message ID: @.>

I reverted till 880f820 the situation is better, but build fails with:

Some required builds logged failures:
- LeanCopilotTests.PremiseSelection
- LeanCopilotTests.ModelAPIs