Skip to content

Commit 781ffbb

Browse files
authored
Fix opam line for vsrocq, shorten rocq-lsp
1 parent f2c5b75 commit 781ffbb

File tree

1 file changed

+3
-19
lines changed

1 file changed

+3
-19
lines changed

src/rocqproverorg_frontend/pages/install.eml

+3-19
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ Layout.render
119119
To use it, you need to install the corresponding language server. Using opam, you can install it with the following command:
120120
</p>
121121

122-
<%s! Copy_to_clipboard.small_code_snippet ~id:"install-vsrocq" "opam install vsrocq-language-server" %>
122+
<%s! Copy_to_clipboard.small_code_snippet ~id:"install-vsrocq" "opam install vscoq-language-server" %>
123123

124124
<p>
125125
Starting from version 2025.01, the language server should already be installed if you installed the <a href="/platform">Rocq Platform</a>.
@@ -135,24 +135,8 @@ Layout.render
135135
</li>
136136
<li>
137137
<p>
138-
<a href="https://github.com/ejgallego/coq-lsp">Rocq LSP</a> is an alternative language server and VS Code extension for the Rocq Prover.
139-
It is available in the <a href="https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp">Visual Studio Code Marketplace</a>
140-
and on <a href="https://open-vsx.org/extension/ejgallego/coq-lsp">Open VSX</a>.
141-
To use it, you need to install the corresponding language server. Using opam, you can install it with the following command:
142-
</p>
143-
144-
<%s! Copy_to_clipboard.small_code_snippet ~id:"install-coq-lsp" "opam install coq-lsp" %>
145-
146-
<p>
147-
Starting from version 2025.01, the language server should already be installed if you installed the <a href="/platform">Rocq Platform</a>.
148-
</p>
149-
150-
<p>
151-
The language server is also available as a <a href="https://search.nixos.org/packages?show=coqPackages.coq-lsp">Nix package</a>.
152-
</p>
153-
154-
<p>
155-
For now, <a href="https://repology.org/project/coq-lsp/versions">Rocq LSP</a> 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).
138+
<a href="https://github.com/ejgallego/coq-lsp">Rocq LSP</a> is an alternative language server and VS Code extension for the Rocq Prover featuring
139+
hybrid Rocq/markdown document support.
156140
</p>
157141
</li>
158142
<li>

0 commit comments

Comments
 (0)