-
|
Hi, I have potentially an infinite number of theorems to trace with LeanDojo. Some of these can be successfully compiled, while others cannot. I am wondering if LeanDojo will tolerate theorems that cannot be compiled through? |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment
-
|
When tracing a repo, LeanDojo requires the repo can be built successfully by However, when using LeanDojo to interact with Lean through commands (see the end of https://github.com/lean-dojo/LeanDojo/blob/main/scripts/demo-lean4.ipynb), it's possible to enter a theorem that cannot be compiled and retrieve the error message from LeanDojo. That part of LeanDojo is experimental, but feel free to let us know if you run into problems. |
Beta Was this translation helpful? Give feedback.
When tracing a repo, LeanDojo requires the repo can be built successfully by
lake build. So it cannot have theorems that cannot be compiled.However, when using LeanDojo to interact with Lean through commands (see the end of https://github.com/lean-dojo/LeanDojo/blob/main/scripts/demo-lean4.ipynb), it's possible to enter a theorem that cannot be compiled and retrieve the error message from LeanDojo. That part of LeanDojo is experimental, but feel free to let us know if you run into problems.