Failing to get mathlib4 #48
Unanswered
AndreSlavescu
asked this question in
Q&A
Replies: 1 comment
-
Did you try set the |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Hello,
I am trying to run the retriever example with the following:
python retrieval/main.py predict --config retrieval/confs/cli_lean4_random.yaml --ckpt_path "my path"
I saved the model checkpoints locally for the following model:
kaiyuy/leandojo-lean4-retriever-byt5-small
And was able to get passed the _load_data stage where the examples are being loaded. After that stage where I get the following error:
Request GET /repos/leanprover-community/mathlib4 failed with 403: rate limit exceeded
Setting next backoff to 970.904135s
Beta Was this translation helpful? Give feedback.
All reactions