diff --git a/src/rocqproverorg_frontend/pages/install.eml b/src/rocqproverorg_frontend/pages/install.eml index 8cd9675b..fce12cd2 100644 --- a/src/rocqproverorg_frontend/pages/install.eml +++ b/src/rocqproverorg_frontend/pages/install.eml @@ -135,24 +135,8 @@ Layout.render
- Rocq LSP is an alternative language server and VS Code extension for the Rocq Prover. - It is available in the Visual Studio Code Marketplace - and on Open VSX. - To use it, you need to install the corresponding language server. Using opam, you can install it with the following command: -
- - <%s! Copy_to_clipboard.small_code_snippet ~id:"install-coq-lsp" "opam install coq-lsp" %> - -- Starting from version 2025.01, the language server should already be installed if you installed the Rocq Platform. -
- -- The language server is also available as a Nix package. -
- -- For now, Rocq LSP is not available in all Linux distributions that have the Rocq Prover. If you have used your Linux distribution's package manager to install the Rocq Prover and it does not include the language server, you can fall back to using VsCoq Legacy (see below). + Rocq LSP is an alternative language server and VS Code extension for the Rocq Prover featuring +hybrid Rocq/markdown document support.
- Rocq LSP is an alternative language server and VS Code extension for the Rocq Prover. - It is available in the Visual Studio Code Marketplace - and on Open VSX. - To use it, you need to install the corresponding language server. Using opam, you can install it with the following command: -
- - <%s! Copy_to_clipboard.small_code_snippet ~id:"install-coq-lsp" "opam install coq-lsp" %> - -- Starting from version 2025.01, the language server should already be installed if you installed the Rocq Platform. -
- -- The language server is also available as a Nix package. -
- -- If you have used Homebrew to install the Rocq Prover, there is no language server available yet. You can fall back to using VsCoq Legacy (see below). + Rocq LSP is an alternative language server and VS Code extension for the Rocq Prover featuring +hybrid Rocq/markdown document support.
+ Rocq LSP is an alternative language server and VS Code extension for the Rocq Prover featuring +hybrid Rocq/markdown document support. +