Issue with demo-lean3.ipynb when creating LeanGitRepo

[ahayat16]

Description When trying to use either demo-lean3.ipynb second cell or last cells of generate-benchmark-lean3.ipynb concerning MiniF2F and ProofNet it fails, apparently because lean-toolchain does not exist (see below).

For instance, when running the first two cells of demo-lean3.ipynb:

from lean_dojo import *

repo = LeanGitRepo( "https://github.com/zhangir-azerbayev/ProofNet", "e8645aa830ce17c33a8b8482a8195f0f97d6a74a", )

repo

gets

---

HTTPError Traceback (most recent call last) Cell In[3], line 1 ----> 1 repo = LeanGitRepo( 2 "https://github.com/zhangir-azerbayev/ProofNet", 3 "e8645aa830ce17c33a8b8482a8195f0f97d6a74a", 4 ) 6 repo

File :5, in init(self, url, commit)

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py:438, in LeanGitRepo.__post_init__(self) 436 lean_version = self.commit 437 else: --> 438 config = self.get_config("lean-toolchain") 439 lean_version = get_lean4_commit_from_config(config) 440 v = get_lean4_version_from_config(config["content"])

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py:577, in LeanGitRepo.get_config(self, filename, num_retries) 575 """Return the repo's files.""" 576 config_url = self._get_config_url(filename) --> 577 content = read_url(config_url, num_retries) 578 if filename.endswith(".toml"): 579 return toml.loads(content)

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/utils.py:202, in read_url(url, num_retries) 200 except Exception as ex: 201 if num_retries <= 0: --> 202 raise ex 203 num_retries -= 1 204 logger.debug(f"Request to {url} failed. Retrying...")

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/utils.py:198, in read_url(url, num_retries) 196 while True: 197 try: --> 198 with urllib.request.urlopen(url) as f: 199 return f.read().decode() 200 except Exception as ex:

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/urllib/request.py:216, in urlopen(url, data, timeout, cafile, capath, cadefault, context) 214 else: 215 opener = _opener --> 216 return opener.open(url, data, timeout)

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/urllib/request.py:525, in OpenerDirector.open(self, fullurl, data, timeout) 523 for processor in self.process_response.get(protocol, []): 524 meth = getattr(processor, meth_name) --> 525 response = meth(req, response) 527 return response

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/urllib/request.py:634, in HTTPErrorProcessor.http_response(self, request, response) 631 # According to RFC 2616, "2xx" code indicates that the client's 632 # request was successfully received, understood, and accepted. 633 if not (200 <= code < 300): --> 634 response = self.parent.error( 635 'http', request, response, code, msg, hdrs) 637 return response

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/urllib/request.py:563, in OpenerDirector.error(self, proto, args) 561 if http_err: 562 args = (dict, 'default', 'http_error_default') + orig_args --> 563 return self._call_chain(args)

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/urllib/request.py:496, in OpenerDirector._call_chain(self, chain, kind, meth_name, args) 494 for handler in handlers: 495 func = getattr(handler, meth_name) --> 496 result = func(args) 497 if result is not None: 498 return result

File ~/opt/anaconda3/envs/ReProver/lib/python3.10/urllib/request.py:643, in HTTPDefaultErrorHandler.http_error_default(self, req, fp, code, msg, hdrs) 642 def http_error_default(self, req, fp, code, msg, hdrs): --> 643 raise HTTPError(req.full_url, code, msg, hdrs, fp)

[ahayat16]

"because lean-toolchain does not exist" -> means https://raw.githubusercontent.com/zhangir-azerbayev/ProofNet/e8645aa830ce17c33a8b8482a8195f0f97d6a74a/lean-toolchain does not exist, but https://raw.githubusercontent.com/zhangir-azerbayev/ProofNet/e8645aa830ce17c33a8b8482a8195f0f97d6a74a/leanpkg.toml does

[yangky11]

The current version of LeanDojo has dropped Lean 3 support. I'll remove these files related to Lean 3.

Since Lean 3 is deprecated, we strongly support using Lean 4. However, if you really need to use Lean 3, please try the legacy branch.

[ahayat16]

Very clear, thanks !