search

lean-dojo / LeanCopilot

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

CI fails due to a model downloading error #80

Closed Peiyang-Song closed 5 months ago

Peiyang-Song commented 5 months ago

CI recently fails due to a model downloading error. Cannot reproduce it in any OS. Will look more into it.

Here is a sample CI log.