From b3992e76e85dc9f80210264438d43d7737383311 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 16:27:48 +0100 Subject: [PATCH 1/4] Unify Rocq CI opam setup --- README.md | 1 + docs/DEVELOPMENT.md | 1 + docs/TESTING.md | 2 ++ tests/setup-rocq-opam.sh | 12 +++++++++--- tests/test-beam-wrapper-rocq.sh | 33 ++++++++++++++++++++++++++++----- tests/test-broker-fast.sh | 1 - tests/test-broker-rocq.sh | 20 +++++--------------- 7 files changed, 46 insertions(+), 24 deletions(-) diff --git a/README.md b/README.md index cc0a3717..2f45f444 100644 --- a/README.md +++ b/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 ``` diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index 0679dbf9..3a01bbff 100644 --- a/docs/DEVELOPMENT.md +++ b/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` diff --git a/docs/TESTING.md b/docs/TESTING.md index 99503e89..c3b51e08 100644 --- a/docs/TESTING.md +++ b/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 project-local `coq-lsp` discovery - 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, diff --git a/tests/setup-rocq-opam.sh b/tests/setup-rocq-opam.sh index 6a047d7c..390d56a4 100755 --- a/tests/setup-rocq-opam.sh +++ b/tests/setup-rocq-opam.sh @@ -8,11 +8,17 @@ 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 diff --git a/tests/test-beam-wrapper-rocq.sh b/tests/test-beam-wrapper-rocq.sh index 10675dde..7363eaff 100755 --- a/tests/test-beam-wrapper-rocq.sh +++ b/tests/test-beam-wrapper-rocq.sh @@ -10,6 +10,7 @@ cd "$(dirname "$0")/.." beam_script="$PWD/scripts/lean-beam" rocq_cmd="${BEAM_ROCQ_CMD:-}" +path_rocq_cmd="" if [ ! -x "$beam_script" ]; then echo "missing lean-beam wrapper at $beam_script" >&2 @@ -17,7 +18,11 @@ if [ ! -x "$beam_script" ]; then fi if [ -z "$rocq_cmd" ]; then - echo "missing BEAM_ROCQ_CMD for Rocq wrapper test" >&2 + path_rocq_cmd="$(command -v coq-lsp || true)" +fi + +if [ -z "$rocq_cmd" ] && [ -z "$path_rocq_cmd" ]; then + echo "missing coq-lsp; set BEAM_ROCQ_CMD or install it in PATH" >&2 exit 1 fi @@ -42,7 +47,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 +71,29 @@ 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 + mkdir -p "$tmp_repo/tests/rocq/Minimal/_opam/bin" + ln -sf "$path_rocq_cmd" "$tmp_repo/tests/rocq/Minimal/_opam/bin/coq-lsp" + "$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 ) diff --git a/tests/test-broker-fast.sh b/tests/test-broker-fast.sh index 65ac10ee..f3e5621b 100644 --- a/tests/test-broker-fast.sh +++ b/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 diff --git a/tests/test-broker-rocq.sh b/tests/test-broker-rocq.sh index f532f7f7..4417bd92 100644 --- a/tests/test-broker-rocq.sh +++ b/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 From dc608f09245d46a1815276ae324f4fd5cbed1496 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 16:36:24 +0100 Subject: [PATCH 2/4] Cache Rocq CI dependencies via setup-ocaml --- .github/workflows/ci.yml | 8 ++++++-- tests/rocq-ci.opam | 9 +++++++++ tests/setup-rocq-opam.sh | 2 +- 3 files changed, 16 insertions(+), 3 deletions(-) create mode 100644 tests/rocq-ci.opam diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2a38b422..f397a9bb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -97,9 +97,13 @@ jobs: uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: 4.14.2 + 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 Tooling - run: bash tests/setup-rocq-opam.sh + - 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 diff --git a/tests/rocq-ci.opam b/tests/rocq-ci.opam new file mode 100644 index 00000000..941e462e --- /dev/null +++ b/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"} +] diff --git a/tests/setup-rocq-opam.sh b/tests/setup-rocq-opam.sh index 390d56a4..98ce3d8f 100755 --- a/tests/setup-rocq-opam.sh +++ b/tests/setup-rocq-opam.sh @@ -26,4 +26,4 @@ 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 From 9fffc13275c7f40406e6a14835885c5bbee20f14 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 16:47:04 +0100 Subject: [PATCH 3/4] Add PATH fallback for Rocq LSP --- Beam/Cli.lean | 8 +++++++- docs/TESTING.md | 2 +- tests/test-beam-wrapper-rocq.sh | 9 +-------- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/Beam/Cli.lean b/Beam/Cli.lean index e32b2423..e54339e2 100644 --- a/Beam/Cli.lean +++ b/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 diff --git a/docs/TESTING.md b/docs/TESTING.md index c3b51e08..e6fdb126 100644 --- a/docs/TESTING.md +++ b/docs/TESTING.md @@ -96,7 +96,7 @@ correctness regression, not yet a performance benchmark. - 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 project-local `coq-lsp` discovery + 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, diff --git a/tests/test-beam-wrapper-rocq.sh b/tests/test-beam-wrapper-rocq.sh index 7363eaff..ce500010 100755 --- a/tests/test-beam-wrapper-rocq.sh +++ b/tests/test-beam-wrapper-rocq.sh @@ -10,18 +10,13 @@ cd "$(dirname "$0")/.." beam_script="$PWD/scripts/lean-beam" rocq_cmd="${BEAM_ROCQ_CMD:-}" -path_rocq_cmd="" if [ ! -x "$beam_script" ]; then echo "missing lean-beam wrapper at $beam_script" >&2 exit 1 fi -if [ -z "$rocq_cmd" ]; then - path_rocq_cmd="$(command -v coq-lsp || true)" -fi - -if [ -z "$rocq_cmd" ] && [ -z "$path_rocq_cmd" ]; then +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 @@ -74,8 +69,6 @@ rsync -a \ 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 - mkdir -p "$tmp_repo/tests/rocq/Minimal/_opam/bin" - ln -sf "$path_rocq_cmd" "$tmp_repo/tests/rocq/Minimal/_opam/bin/coq-lsp" "$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 From fbf8036f3be59ff17e72d60cc46e5f264fc269b9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 16:54:26 +0100 Subject: [PATCH 4/4] Enable dune cache for Rocq CI --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f397a9bb..cb64ab6e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -97,6 +97,7 @@ jobs: uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: 4.14.2 + dune-cache: true opam-repositories: | default: git+https://github.com/ocaml/opam-repository.git coq-released: https://coq.inria.fr/opam/released