feat: lake exe function (#76)

[quinn-dougherty]

Inspired by lsp-rust-analyzer-run, lean4-lake-exe parses out executable names from lakefile.lean and runs them in their dedicated buffer.

[quinn-dougherty]

it's come to my attention that unquoted executable names are legal in lakefile, and i've struggled with getting them right a little. converted to draft till i figure that out.

additionally: if anyone thinks i shouldn't dump this whole diff into the lean4-lake.el file, let me know, happy to do something else!

[mekeor]

Thanks for your interest in contribution and for the interesting idea. Unfortunately, I'm not convinced of the approach to use regular expressions to extract the executable names. Especially now that Lake uses TOML by default and lakefile.lean is dedicated towards more experienced users.

I think it'd be best if Lake itself offered a command like lake list-executables that would output the executable names in a suitable format. We could then use its output from Emacs.

[mekeor]

I'd like to close this PR due to the lack of a feasibly globally valid approach to determine the executable names. If you are very motivated, I suggest you contribute a lake list-executables command or similar to Lake itself first, before revisiting the development of this feature.

[mekeor]

Feel free to reopen if you disagree.

[quinn-dougherty]

indeed-- I started this back when the « ticks were default in the lakefile.lean, and before I realized toml was an option / before they made toml default. I agree with your thoughts! thanks a ton btw for coming in and attending the issues, I super appreciate it.