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 <#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: ***@***.***>

[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

[yangky11]

I just updated LeanCopilot to support recent versions of Lean/mathlib. Could you please try again and see if the issue still persists.

This is what I got:

[robomotic]

Great thanks, will attempt tomorrow. Cheers.

…

On Tue, 24 Dec 2024, 21:26 Kaiyu Yang, ***@***.***> wrote: I just updated LeanCopilot to support recent versions of Lean/mathlib. Could you please try again and see if the issue still persists. This is what I got: image.png (view on web) <https://github.com/user-attachments/assets/961b0047-af28-42c2-a3e9-cb34a7833322> — Reply to this email directly, view it on GitHub <#127 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AACNEPFOQGVXDPSNLP4ZCCT2HHGO5AVCNFSM6AAAAABQHPROUOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKNRRGQ2TQOJYHE> . You are receiving this because you authored the thread.Message ID: ***@***.***>