Failing to get mathlib4

[AndreSlavescu]

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

[yangky11]

Did you try set the GITHUB_ACCESS_TOKEN environment variable as mentioned in LeanDojo's requirements?