lean-dojo / LeanDojo

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

Python 3.9 syntax issue #129

Closed AG161 closed 5 months ago

AG161 commented 5 months ago

Description Not sure if this is worth mentioning but I think the current version uses syntax for Python 3.10+ (e.g. def cleanse_string(s: str | Path), might be worth adjusting the requirements in the readme or using 3.9+ friendly syntax.

Logs in Debug Mode

(dj) agittis@trurl:~/Dojo$ echo $VERBOSE
1
(dj) agittis@trurl:~/Dojo$ python
Python 3.9.5 (default, Nov 23 2021, 15:27:38) 
[GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from lean_dojo import *
2024-01-19 15:07:09.393 | DEBUG    | lean_dojo.constants:<module>:67 - Using GitHub personal access token for authentication
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/agittis/Dojo/dj/lib/python3.9/site-packages/lean_dojo/__init__.py", line 2, in <module>
    from .data_extraction.trace import (
  File "/home/agittis/Dojo/dj/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py", line 22, in <module>
    from .lean import LeanGitRepo
  File "/home/agittis/Dojo/dj/lib/python3.9/site-packages/lean_dojo/data_extraction/lean.py", line 40, in <module>
    def cleanse_string(s: str | Path) -> str:
TypeError: unsupported operand type(s) for |: 'type' and 'type'
>>> 

Platform Information

yangky11 commented 5 months ago

Fixed in v1.5.1