In-source evaluation of expressions (and in-source unit tests)

I don’t think # or any special keyword is necessary or desirable (except for the purpose of imitating Lean syntax); like in worksheets, just top-level expression can be enough. If you wanted them not to be evaluated, you would have to comment them out anyway (regardless of #).

I’m not sure why you’re not satisfied with worksheets though? It solves all the problems you hate. I ported hundreds of interactive Dr. Racket files with unit tests to Scala worksheets successfully and satisfactorily. Thanks to the Doodle library I even ported the interactive animations :smiley: Does the file extension bother you that much? You can always change it back to .scala later if you want :smiley: I’ve done so hundreds of times. If it’s for non-educational purposes, you wouldn’t want to leave those evaluations polluting the file anyway right? And for educational purposes you’d want to leave them there.

Probably nothing is necessary or possible in the compiler; Lean was designed as an interactive prover from the beginning, aimed at non-programmers and mathematicians, and not for building applications; so its compiler must be fundamentally different than Scala’s. My understanding is that Lean has a “kernel” that implements the CoC type-checker, and everything else around it (VS Code extension, etc.) interacts with this kernel. Essentially, every Lean source file is an “interactive worksheet” in VS Code. It evaluates even if you don’t use #eval or #check or #guard. The kernel will evaluate the types where you place your mouse cursor, at all times. To get an executable binary you have to do additional stuff on the command line (with lake build), which also uses the kernel but differently.

Also I would have to say that Lean’s “everything is a worksheet” can sometimes be an awful experience. It can consume too much CPU/RAM or crash, or become very slow / unresponsive. Non-interactive, performance aware Lean code (in Mathlib for example) is unreadable to humans. In my educational code, I make a clear distinction between “lightweight, interactive exploration with worksheets / scripts” (.worksheet.sc or .sc) and “more serious, possibly performance heavy code to be run” (.scala).

Probably best approach is to ask @tgodzik and maybe raise a Metals feature request, you could probably implement it as a Metals feature or a VS Code extension / add-on; basically all you need is to look at how worksheets are done and hack it so that it can work for .scala files.