search

lean-dojo / LeanDojo

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

LeanDojo should not be run as root #191

Closed yyyhz closed 1 month ago

yyyhz commented 1 month ago 
raise RuntimeError("LeanDojo should not be run as root.")

RuntimeError: LeanDojo should not be run as root.

I wonder if I can use LeanDojo with root

yangky11 commented 1 month ago

What is the complete error message? Are you using the most recent version?