search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
276 stars 26 forks source link

Show file progress as a diagnostic while it occurs. #253

Closed Julian closed 2 years ago

Julian commented 2 years ago

Helps make sure someone using e.g. vim.diagnostic.goto_next notices that the file isn't ready yet.

Closes: https://github.com/Julian/lean.nvim/issues/252

Julian commented 2 years ago

(The tests seem a bit flaky again locally, will investigate, but pinging the both of you in case you have an opinion on how well this works for you.)

gebner commented 2 years ago

LGTM. This is much less annoying than I'd feared.

rish987 commented 2 years ago

LGTM as well, thank you! Yeah the tests in general need some work (I've been busy reading lately but will get back to #250 soon).