running Lean from the command line

[cipher1024]

Instead of calling lean my_file.lean and having #eval main in your source file, I recommend you call Lean lean --run my_file.lean without the #eval statement. It will run your main function

[agentultra]

Thanks, agreed -- will update that ASAP; or a PR is always welcome.