Unify Rocq CI opam setup

.github/workflows/ci.yml

@@ -97,9 +97,14 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: 4.14.2
-
-      - name: Install Rocq Tooling
-        run: bash tests/setup-rocq-opam.sh
+          dune-cache: true
+          opam-repositories: |
+            default: git+https://github.com/ocaml/opam-repository.git
+            coq-released: https://coq.inria.fr/opam/released
+          opam-local-packages: tests/rocq-ci.opam
+
+      - name: Install Rocq CI Dependencies
+        run: opam install -y ./tests/rocq-ci.opam --deps-only
 
       - name: Broker Rocq Test
         run: bash tests/test-broker-rocq.sh

Beam/Cli.lean

@@ -636,13 +636,19 @@ private def leanBin (root : System.FilePath) : IO String := do
 private def rocqCandidates (root : System.FilePath) : List System.FilePath :=
   [root / "_opam" / "bin" / "coq-lsp", root / "_opam" / "_opam" / "bin" / "coq-lsp"]
 
+private def pathCmd? (cmd : String) : IO (Option String) := do
+  try
+    return some (← readCmdTrim "sh" #["-c", s!"command -v {shellQuote cmd}"])
+  catch _ =>
+    return none
+
 private def maybeRocqCmd (root : System.FilePath) : IO (Option String) := do
   for candidate in rocqCandidates root do
     if ← candidate.pathExists then
       return some candidate.toString
   match ← IO.getEnv "BEAM_ROCQ_CMD" with
   | some cmd => pure (some cmd)
-  | none => pure none
+  | none => pathCmd? "coq-lsp"
 
 private def rocqCmd (root : System.FilePath) : IO String := do
   match ← maybeRocqCmd root with

README.md

@@ -135,6 +135,7 @@ Broker and wrapper suites:
 ```bash
 bash tests/test-broker-fast.sh
 bash tests/test-broker-slow.sh
+bash tests/test-broker-rocq.sh
 bash tests/test-broker.sh
 bash scripts/lint-shell.sh
 ```

docs/DEVELOPMENT.md

@@ -70,6 +70,7 @@ Preferred maintainer entrypoints:
 
 - broker protocol / stream / barrier changes: `bash tests/test-broker-fast.sh`
 - wrapper / install / bundle-resolution changes: `bash tests/test-broker-slow.sh`
+- Rocq broker / wrapper changes: `bash tests/test-broker-rocq.sh`
 - risky local install or wrapper validation: `bash scripts/validate-defensive.sh`
 - shell changes: `bash scripts/lint-shell.sh`
 

docs/TESTING.md

@@ -95,6 +95,8 @@ correctness regression, not yet a performance benchmark.
   and request-stream contract changes; this is the quickest broker signal
 - add [tests/test-broker-slow.sh](../tests/test-broker-slow.sh) when the change touches wrapper,
   install, or bundle-resolution behavior
+- use [tests/test-broker-rocq.sh](../tests/test-broker-rocq.sh) for Rocq broker and wrapper
+  coverage, including `coq-lsp` discovery from project-local `_opam` roots and the active PATH
 - use [tests/test-broker.sh](../tests/test-broker.sh) to execute both suites together before
   landing a broader broker-facing change
 - use [scripts/lint-shell.sh](../scripts/lint-shell.sh) when you change shell wrappers, installer,

tests/rocq-ci.opam

@@ -0,0 +1,9 @@
+opam-version: "2.0"
+synopsis: "CI-only Rocq dependencies for lean-beam broker tests"
+maintainer: "Emilio J. Gallego Arias"
+license: "Apache-2.0"
+depends: [
+  "rocq-core" {= "9.1.1"}
+  "rocq-stdlib"
+  "coq-lsp" {= "0.2.5+9.1"}
+]

tests/setup-rocq-opam.sh

@@ -8,16 +8,22 @@ set -euo pipefail
 
 cd "$(dirname "$0")/.."
 
-if [ ! -d "_opam/_opam" ]; then
-  opam switch create ./_opam 4.14.2
+if ! command -v opam > /dev/null 2>&1; then
+  echo "missing opam; install it first or run under ocaml/setup-ocaml" >&2
+  exit 1
 fi
 
-eval "$(opam env --switch=./_opam --set-switch)"
+if ! opam switch show > /dev/null 2>&1; then
+  echo "missing active opam switch; run under ocaml/setup-ocaml or select a switch first" >&2
+  exit 1
+fi
+
+eval "$(opam env)"
 
 if ! opam repo list --short | grep -qx 'coq-released'; then
   opam repo add coq-released https://coq.inria.fr/opam/released
 fi
 
 opam update
 
-opam install -y rocq-core.9.1.1 rocq-stdlib coq-lsp.0.2.5+9.1
+opam install -y ./tests/rocq-ci.opam --deps-only

tests/test-beam-wrapper-rocq.sh

@@ -16,8 +16,8 @@ if [ ! -x "$beam_script" ]; then
   exit 1
 fi
 
-if [ -z "$rocq_cmd" ]; then
-  echo "missing BEAM_ROCQ_CMD for Rocq wrapper test" >&2
+if [ -z "$rocq_cmd" ] && ! command -v coq-lsp > /dev/null 2>&1; then
+  echo "missing coq-lsp; set BEAM_ROCQ_CMD or install it in PATH" >&2
   exit 1
 fi
 
@@ -42,7 +42,11 @@ remove_owned_tmp_tree() {
 
 cleanup() {
   if [ -d "$tmp_repo/tests/rocq/Minimal" ]; then
-    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true
+    if [ -n "$rocq_cmd" ]; then
+      BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true
+    else
+      "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true
+    fi
   fi
   remove_owned_tmp_tree "$tmp_repo"
 }
@@ -62,15 +66,27 @@ rsync -a \
     echo "expected lake build beam-cli not to prebuild Beam daemon helper executables" >&2
     exit 1
   fi
-  BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
+  if [ -n "$rocq_cmd" ]; then
+    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
+  else
+    "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
+  fi
   if [ -x ".lake/build/bin/beam-daemon" ] || [ -x ".lake/build/bin/beam-client" ]; then
     echo "expected doctor rocq to remain read-only and not build Beam daemon helpers" >&2
     exit 1
   fi
-  BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq > /dev/null
+  if [ -n "$rocq_cmd" ]; then
+    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq > /dev/null
+  else
+    "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq > /dev/null
+  fi
   if [ ! -x ".lake/build/bin/beam-daemon" ] || [ ! -x ".lake/build/bin/beam-client" ]; then
     echo "expected rocq CLI startup to build missing Beam daemon helpers on demand" >&2
     exit 1
   fi
-  BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null
+  if [ -n "$rocq_cmd" ]; then
+    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null
+  else
+    "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null
+  fi
 )

tests/test-broker-fast.sh

@@ -17,7 +17,6 @@ lake build \
   beam-daemon-smoke-test \
   beam-daemon-save-stream-test \
   beam-daemon-request-stream-test \
-  beam-daemon-rocq-smoke-test \
   > /dev/null
 
 .lake/build/bin/beam-daemon-smoke-test > /dev/null

tests/test-broker-rocq.sh

@@ -16,25 +16,15 @@ lake build \
   beam-daemon-rocq-smoke-test \
   > /dev/null
 
-ROCQ_LSP=""
-for candidate in "_opam/bin/coq-lsp" "_opam/_opam/bin/coq-lsp"; do
-  if [ -x "$candidate" ]; then
-    ROCQ_LSP="$candidate"
-    break
-  fi
-done
-
-if [ -z "$ROCQ_LSP" ]; then
+eval "$(opam env)"
+
+if ! command -v coq-lsp > /dev/null 2>&1; then
   echo "missing coq-lsp; run tests/setup-rocq-opam.sh first" >&2
   exit 1
 fi
 
-if [ -d "_opam/_opam" ]; then
-  eval "$(opam env --switch=./_opam --set-switch)"
-fi
-
 echo "[broker-rocq] wrapper tests"
-BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" bash tests/test-beam-wrapper-rocq.sh > /dev/null
+bash tests/test-beam-wrapper-rocq.sh > /dev/null
 
 echo "[broker-rocq] smoke test"
-BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" .lake/build/bin/beam-daemon-rocq-smoke-test > /dev/null
+.lake/build/bin/beam-daemon-rocq-smoke-test > /dev/null