search

lean-dojo / LeanDojo

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

Reduce Memory Usage When Tracing Repos #124

Closed yangky11 closed 4 months ago

yangky11 commented 6 months ago

Sometimes tracing the repo can take 100 GB memory: https://github.com/lean-dojo/LeanDojo/issues/119 https://github.com/lean-dojo/LeanDojo/issues/41.

yangky11 commented 5 months ago

https://github.com/lean-dojo/LeanDojo/discussions/116

yangky11 commented 5 months ago

PR: https://github.com/lean-dojo/LeanDojo/pull/133