Evaluate expression without "modern" editor

Stream: general

[Jon Kleiser]

My favorite Mac editor, BBEdit, does not support a language server. So when the Lean docs tells me "To ask Lean to evaluate an expression, write #eval before it in your editor", it makes no sense. Is there another way to quickly evaluate expressions?

[Shreyas Srinivas]

When I run lake build, I get the lines of #eval printed among the rest of the output (this being the key pain point).

[Shreyas Srinivas]

In general using vscode (or neovim/emacs) is the way to get the best possible experience

[Jireh Loreaux]

Jon, the key thing about Lean (or at least, one of the major ones) is its interactivity. You need to use an editor with proper support (VSCode, Emacs, NeoVim).