Prevent execution of `#eval` during editing

Stream: lean4

[Mac]

Is there a way to print heavy duty #evals (i.e. side-effect commands) from running in the editor (i.e. only running when the file is directly run with lean)?

[Mario Carneiro]

you can use def main := instead of #eval

[Mac]

main isn't run by lean though? main is only used in the built executable? I want to run the #eval at interpretation time but not editing time.

[Mario Carneiro]

won't that make them diverge?

[Mario Carneiro]

#eval can modify the environment

[Mac]

yes, but that's the point. If #eval is doing heavy duty IO work like compiling code or building a project, I don't want that run every time the editor is opened or refreshed.