Open Issues Need Help
View All on GitHub Remote cache doesn't work in Windows due to DOS style path about 2 months ago
AI Summary: Fix the LeanDojo Python library's remote cache functionality on Windows by correcting the path handling to accommodate backslashes in URLs. This likely involves replacing `os.path` with `pathlib` to ensure proper URL construction and handling of different operating system path separators.
Complexity:
3/5
enhancement help wanted
Tool for data extraction and interacting with Lean programmatically.
Python
#lean#lean4#machine-learning#theorem-proving