search

lean-dojo / LeanDojo

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

build_lean4_repo.py crashes with Lean v4.3.0 #118

Closed tonyxty closed 7 months ago

tonyxty commented 7 months ago

Description ... because the is_new_version function will crash when the argument is "4.3.0".

Detailed Steps to Reproduce the Behavior Build any repo with toolchain specified as "v4.3.0"

Logs in Debug Mode

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/tony/src/lean-dojo/LeanDojo/src/lean_dojo/data_extraction/build_lean4_repo.py", line 137, in is_new_version
    return rc >= 2
UnboundLocalError: local variable 'rc' referenced before assignment

Platform Information