Mac Malone

@semorrison Lean/Lake does add new keywords as time progresses and those new keywords would then break packages with those names. A possibly better solution (which was part of #3174) is...

Related discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Omit.20compilation.20and.20run.20the.20executable.20binary.20in.20the.20.2Elake/near/468564582

With this suggestion, should it still print an error / return exit code 1 or should it just produce the listing and exit normally?

@semorrison > (If there were `lake describe exe` or something, then _that_ should exit normally.) There is `lake help exe`, but loading the workspace as part of help seems like...

@sullyj3 It could, but there are some things to consider: 1. Unlike `cargo run`, arguments are passed without a `--` separator, so a `lake exe` with a named exe would...

> I don't think anything should ever be both a draft and will-merge-soon, @semorrison Definitely! That was just me forgetting to mark it ready for review. 🤦‍♂️

@Kha Right now, this is just for interactive editing, not for building the binaries or shared libraries, so we do not need those options at the moment.

@Kha > Okay, I would not have expected that to be a desirable intermediate state if it forces me to redo the build in cmake whenever I want to actually...

I am flummoxed by the linker errors in the CMake build of stage0 Lake. It builds successfully on my machine.

@Kha > It wasn't clear to me why the additional lakefile.tomls in the root and in tests/ are necessary, so I've removed them for now. They are necessary for the...