search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
70 stars 28 forks source link

`lean4-lake-exe` function #76

Open quinn-dougherty opened 3 months ago

quinn-dougherty commented 3 months ago

I'm a huge fan of lsp-rust-analyzer-run, which

  1. opens a menu of executables and test suites
  2. when I select one, runs that executable in a dedicated buffer.

Would be awesome to have this for lake!

mekeor commented 2 days ago

This sounds interesting. Could you perhaps share a screenshot of the menu that lsp-rust-analyzer-run opens and also the dedicated buffer after selection?