描述
Coq implements a custom XML protocol described here to step through proofs, and update the goal and window at each step. Unfortunately, this has the consequence that many of the nice features that are otherwise available to languages going the LSP route are unavailable to Coq. The consumers of this protocol are CoqIDE, VSCoq, and Proof General.
Other proof assistants such as Isabelle/HOL have poor VSCode support and roll their own IDEs. Lean and Agda, in particular, do not suffer from this issue, because it is not a traditional "interactive proof assistant", whence one steps through proofs. In its VSCode extension for Lean, it automatically evaluates the entire buffer and stops at the first error. F* did suffer from this issue, and I happen to be the primary author of its LSP server: the work was stalled because there was no way to step through proofs via LSP.
This is a stark deficiency of the Language Server Protocol, and I feel that we can do better.