search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
552 stars 83 forks source link

Request GET /repos/leanprover/lean4 failed with 403: rate limit exceeded #140

Closed vu-duy-tung closed 7 months ago

vu-duy-tung commented 7 months ago

Description Hi, sometimes, when I run the following code: 

from lean_dojo import *

repo = LeanGitRepo(
    "https://github.com/leanprover-community/mathlib4",
    "3ce43c18f614b76e161f911b75a3e1ef641620ff",
)

theorem = Theorem(repo, "Mathlib/Combinatorics/Catalan.lean", "Tree.treesOfNumNodesEq_card_eq_catalan")

dojo, state_0 = Dojo(theorem).__enter__()
print("\n-----------State 0:----------")
print(state_0.pp)

print("\n-----------State 1:----------")
state_1 = dojo.run_tac(state_0, "induction' n using Nat.case_strong_induction_on with n ih")
print(state_1.pp)

I face a limitation in the number of request which will show

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

Detailed Steps to Reproduce the Behavior I installed the requirements of LeanDojo and tried the demo of LeanDojo with Lean4

Logs in Debug Mode This is not actually a bug, after waiting for the backoff in about 45 minutes, the code is run normally. But it takes a very long time whenever I use LeanDojo.

Platform Information

vu-duy-tung commented 7 months ago

I will close the issue due to setting GITHUB_ACCESS_TOKEN can enhance the number of requests