search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Add an equivalent of refresh file dependencies for Lean 4 #262

Closed Julian closed 2 years ago

Julian commented 2 years ago

We need a command equivalent of lean4.refreshFileDependencies for telling the Lean server to restart the worker for the current file / refresh building imported files.

gebner commented 2 years ago

I've been abusing :e for this.

Julian commented 2 years ago

Probably we should keep telling others that's the "official" way to do it -- the reason to have something else just in case would be for someone (yesterday me) having a BufRead autocmd they're running, in which case hitting :e will keep triggering it unnecessarily.

Maybe doesn't have to be an exact equivalent of refresh file dependencies, could just be we kill + restart an LSP client.

gebner commented 2 years ago

Yeah, the :e is not ideal. You also need to do :w first.

The server expects a didClose followed by a didOpen notification to restart the file worker. Restarting the LSP server is useful as well (and unfortunately not as easy as :LspRestart), but it restarts all the file workers, which is rarely what you want.