You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
Peiyang-Song
changed the title
Cloud release mechanism after recent Lake updates
Problem with the cloud release mechanism after recent Lake updates
Aug 15, 2024
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 thelakefile
and make the process more convenient again.The text was updated successfully, but these errors were encountered: