search

lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean
https://leandojo.org
MIT License
999 stars 92 forks source link

Problem with the cloud release mechanism after recent `Lake` updates #115

Open Peiyang-Song opened 3 months ago

Peiyang-Song commented 3 months ago

After recent Lake updates, we found that the cloud release mechanism is not working as expected. Specifically, on some supported architectures, where Lean Copilot is expected to directly download cloud release instead of re-building, the log indicates that a building still occurs. This does not create any actual bugs because Lean Copilot should be able to build just well on these supported architectures, yet it would be great if we fix the cloud release mechanism in the lakefile and make the process more convenient again.

Peiyang-Song commented 3 months ago

Seems like Issue #117 is related to this problem too.