Running into error with LeanDojo

Stream: lean4

[Shubhra Mishra]

Hello!

I was setting up LeanDojo, and running an example file. I run into an error saying "CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1." I'm not sure how to fix this. What should I do?

image.png

[Scott Morrison]

You likely will need to contact the LeanDojo authors.

(Note that the REPL referred to here is not the official one.)