403: rate limit exceeded errors

[joshuaongg21]

Hello! When I tried to train python retrieval/main.py fit --config retrieval/confs/cli_lean4_random.yaml, I received numerous failed with 403: rate limit exceeded errors, e.g., Request GET /repos/leanprover/lean4 failed with 403: rate limit exceeded, Request GET /repositories/129571436/branches?page=23 failed with 403: rate limit exceeded, and so on. Is this normal, and how can I resolve it?

I have checked

"""Script for training the premise retriever.
"""

print("Starting imports")
import os
import requests
from loguru import logger
print("Core imports done")

github_token = os.getenv('GITHUB_TOKEN')
if github_token:
    headers = {'Authorization': f'token {github_token}'}
    logger.info(f"GitHub token found. Headers: {headers}")
else:
    headers = {}
    logger.warning("No GitHub token found in environment variables.")

from pytorch_lightning.cli import LightningCLI
print("LightningCLI imported")
from retrieval.model import PremiseRetriever
print("PremiseRetriever imported")
from retrieval.datamodule import RetrievalDataModule
print("RetrievalDataModule imported")
print("All imports completed")
class CLI(LightningCLI):
    def add_arguments_to_parser(self, parser) -> None:
        parser.link_arguments("model.model_name", "data.model_name")
        parser.link_arguments("data.max_seq_len", "model.max_seq_len")

it tends to stuck during/after the LightningCLI section

Starting imports
Core imports done
2024-06-22 01:19:33.951 | INFO     | __main__:<module>:13 - GitHub token found. Headers: {'Authorization': 'XXX'}
LightningCLI imported
Request GET /repos/leanprover/lean4 failed with 403: rate limit exceeded
Setting next backoff to 2257.653931s

[yangky11]

Did you set the GITHUB_ACCESS_TOKEN environment following https://github.com/lean-dojo/LeanDojo?tab=readme-ov-file#requirements?

[joshuaongg21]

Hi, yes! I've set
export GITHUB_TOKEN=<personal_access_token>
proceeding with
echo $GITHUB_TOKEN (the token is there!)
curl -H "Authorization: token $GITHUB_TOKEN" https://api.github.com/user
curl -H "Authorization: token $GITHUB_TOKEN" https://api.github.com/rate_limit

for making sure the API key is there. However it still doesnt work and

Request GET /repos/leanprover/lean4 failed with 403: rate limit exceeded
Setting next backoff to 1543.630394s

still occurs

[yangky11]

It's GITHUB_ACCESS_TOKEN instead of GITHUB_TOKEN.