search

lean-dojo / LeanDojo

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

fixing pylance errors: lean.py #56

Closed josojo closed 12 months ago

josojo commented 1 year ago

type checkers like pylance are currently throwing some errors. I want to fix them and then prevent them in the future via CI. This PR fixes them in lean.py

yangky11 commented 1 year ago

Hi,

Thanks for the PR! It would be great if you could share your commands for running the type checker. I can add them to https://leandojo.readthedocs.io/en/latest/developer-guide.html#static-type-checking.

I tried mypy but there were too many errors to fix. Maybe I was not configuring mypy in the right way, or maybe I should just switch to pylance.

josojo commented 1 year ago

Ups, I just saw that you even have a mypy configuration already committed. Then I am fine with using mypy.

Pylance was built on top of pyright:

pip install pyright
pyright ./src/lean_dojo/data_extraction/lean.py

gives me:

pyright ./src/lean_dojo/data_extraction/lean.py 
/Users/josojo/coding/ai/LeanDojo/src/lean_dojo/data_extraction/lean.py
  /Users/josojo/coding/ai/LeanDojo/src/lean_dojo/data_extraction/lean.py:12:6 - error: Import "github.Repository" could not be found in the "python" environment. (reportMissingImports)
1 error, 0 warnings, 0 information

I reduced them from over ten in this PR. The one remaining is not shown by my IDE. Yes, In general, there are over 100 type issues in the project(for pyright and mypy)

Maybe we should first make the mypy.ini settings very loose (setting strict to false etc) and then tackle file by file. Later on, we can then make the configuration more strict.

yangky11 commented 12 months ago

I'm OK with either mypy or pyright. Let me merge this PR to the dev branch first. Later I'll merge it to main after all tests have passed. Thanks!