LeanDojo
LeanDojo copied to clipboard
lean-dojo
Tool for data extraction and interacting with Lean programmatically.
## Description In the `demo-lean4` Jupyter notebook, the code fails to execute starting from the "Interacting with Lean" section. Specifically, the line: ```python dojo, state_0 = Dojo(theorem).__enter__() ``` produces the...
TODOs * Fix tracing repos with lakefile.toml, e.g., [aesop](https://github.com/leanprover-community/aesop)
Changes to support lake projects that aren't at the root of a github repo. Applicable to projects like https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean This is WIP and not ready to merge (e.g., we'd need...
Thanks for open sourcing this tool, it's great! I'd like to use it with projects such as https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean, which has a lake project in a subfolder instead of at the...
**Description** I am trying to trace [the PFR repo on commit 6a5082ee465f9e44cea479c7b741b3163162bb7e](https://github.com/teorth/pfr/tree/6a5082ee465f9e44cea479c7b741b3163162bb7e) using LeanDojo version 2.0.3. However, I am running into the following error: ``` Failed to trace repo LeanGitRepo...
TODO: Make sure the [typechecking CI](https://github.com/lean-dojo/LeanDojo/blob/main/.github/workflows/type_check.yaml) passes.
**Description** I believe the `scripts/generate-benchmark-lean4.ipynb` is buggy. I evaluated the performance of the ReProver premise retriever on a dataset I generated from Mathlib4. I should get a recall of around...
I noticed that all the unicode characters in the dataset are ascii-encoded Seems like you didn't set `ensure_ascii=False`. I wonder if this will affect the performance of premise selection. After...
## Involved Issue Close #196 ## Note - fix some chore typing. - fix subclass call parent factroy method `from_data` or `from_xml`. use Generic[T]. - fix `child[x]` use cast pass...
