From 923099da303a1ac431e597c96d1cf30539fa8b24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Sun, 1 Feb 2026 21:53:06 +0100 Subject: [PATCH] coq.withPackages: document use with language servers Added guidance on installing Rocq language servers when using `coq.withPackages`. #484870 --- doc/languages-frameworks/rocq.section.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/languages-frameworks/rocq.section.md b/doc/languages-frameworks/rocq.section.md index ae1fec87e478..af83d1e3790b 100644 --- a/doc/languages-frameworks/rocq.section.md +++ b/doc/languages-frameworks/rocq.section.md @@ -36,6 +36,8 @@ coq.withPackages ( ) ``` +If you install the `vsrocq-language-server` or `rocq-lsp` server, make sure to list them as part of the above `coq.withPackages` expression instead of installing them separately if you want them to find your Coq/Rocq packages. + ## Rocq packages attribute sets: `rocqPackages` {#rocq-packages-attribute-sets-rocqpackages} The recommended way of defining a derivation for a Rocq library, is to use the `rocqPackages.mkRocqDerivation` function, which is essentially a specialization of `mkDerivation` taking into account most of the specifics of Rocq libraries. The following attributes are supported: