Emilio Jesús Gallego Arias

This is something we inherit from C.J.'s VsCoq 1, I think that VSCoq 2 also uses the same file; maybe we could sync the effort on Zulip to improve this....

Hi @4ever2 , indeed it hasn't been easy to coordinate that; I'd be amazing if you would open a PR updating our definitions! Please don't forget to update the changelog...

@Alizter we can also implement semantic tokens, that should be easy for commands that are not defined in plugins.

Semantic token spec https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_semanticTokens

In order to implement semantic tokens in coq-lsp we need to: - add the different kind of tokens and types to `lang`, maybe to `lang/ast.mli` ? - write a function...

Yup, you can do that even without modifying the server. Add a command that issues the goals request with a payload `command: "Show Proof."`, then you can get the answer...

Hi @audreyseo , that would be extremely welcome; sorry for the incomplete documentation, and thanks for taking the time to submit this issue.

Hi @mseri ! Thanks for your message! First let me summarize how the current WASM support works in jsCoq (work done by @corwin-of-amber) : - we compile OCaml's bytecode interpreter...

This is fixed by #1008 , using Shachar's `ocaml-wasm`. Still, the performance is not the best, it'd be great to try wasm_of_ocaml and see how it goes. I think the...

Thanks for the bug report. To shed some light on this issue, this is mostly due to the way we handle `Range` in Flèche. Flèche uses a range type that...