Closed OctoberFox11 closed 2 weeks ago
I had the same issue, but with lake build
, and not lake env lean --threads 4 --run ExtractData.lean.
I solved it by making sure all the lean files in the directory did not have any errors in them.
(edit: never mind sorry)
It's because fd14c4c8b29cc74a082e5ae6f64c2fb25b28e15e
is too old, and Lean has made quite a few breaking changes since this commit.
You can simply change it to 7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f
. I'll also updating LeanDojo's documentation to reflect this.
Feel free to re-open if the issue still persists.
Description I'm an amateur and I've spent days starting lean_dojo :( My error occurs when trying to run
lean_dojo
with a specific Lean4 repository. The process fails with aCalledProcessError
when attempting to execute thelake env lean --threads 4 --run ExtractData.lean
command.Detailed Steps to Reproduce the Behavior
Use the following code to reproduce the error:
Logs in Debug Mode Command failed with exit status 1
Command output: [0/1] Building Lean4Example
Command stderr:
Platform Information