From 5319be66952711a42be8ad027e9b0681a122efcd Mon Sep 17 00:00:00 2001
From: Daniel Fahey <dpf@helmcontrol.ltd>
Date: Fri, 22 May 2026 22:40:11 +0100
Subject: [PATCH] coq-lsp: add `$OCAMLFIND_DESTDIR` to wrapper `OCAMLPATH`

`wrapProgram` in `installPhase` prepends propagated build inputs'
`$OCAMLPATH` but omits `$OCAMLFIND_DESTDIR`, coq-lsp's own site-lib
containing the compiled serlib `.cmxs` plugins. At runtime Rocq's
plugin loader maps plugin names (e.g. `rocq-runtime.plugins.ltac`) to
serlib adapters (e.g. `coq-lsp.serlib.ltac`) and calls
`Findlib.package_directory()` to locate them. Without coq-lsp's own
output in `OCAMLPATH`, findlib fails and seven "not available" warnings
are emitted on every `.v` file.

`$OCAMLFIND_DESTDIR` is set by the preceding `dune install` invocation.
Prepending it to the wrapper's `OCAMLPATH` ensures coq-lsp can discover
its own serlib plugins at runtime.

Assisted-by: Syzygy(tnxwqvtl)/OpenCode(1.14.48):zai-coding-plan/glm-5.1
---
 pkgs/development/coq-modules/coq-lsp/default.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pkgs/development/coq-modules/coq-lsp/default.nix b/pkgs/development/coq-modules/coq-lsp/default.nix
index 608b674c27b1..e9ed905ff3f5 100644
--- a/pkgs/development/coq-modules/coq-lsp/default.nix
+++ b/pkgs/development/coq-modules/coq-lsp/default.nix
@@ -66,7 +66,7 @@
   installPhase = ''
     runHook preInstall
     dune install -p ${pname} --prefix=$out --libdir $OCAMLFIND_DESTDIR
-    wrapProgram $out/bin/coq-lsp --prefix OCAMLPATH : $OCAMLPATH
+    wrapProgram $out/bin/coq-lsp --prefix OCAMLPATH : $OCAMLFIND_DESTDIR --prefix OCAMLPATH : $OCAMLPATH
     runHook postInstall
   '';