Skip to content

Unify Rocq CI opam setup - #4

Merged
ejgallego merged 4 commits into
mainfrom
codex/rocq-ci-unify-opam
Mar 16, 2026
Merged

Unify Rocq CI opam setup#4
ejgallego merged 4 commits into
mainfrom
codex/rocq-ci-unify-opam

Conversation

@ejgallego

@ejgallego ejgallego commented Mar 16, 2026

Copy link
Copy Markdown
Collaborator

Summary

  • reuse the active opam switch from ocaml/setup-ocaml instead of creating a separate local Rocq switch
  • define Rocq CI dependencies in tests/rocq-ci.opam, install them explicitly with opam install --deps-only, and let setup-ocaml cache the populated switch
  • enable the OCaml action's dune cache for the Rocq CI job
  • make Rocq command resolution and tests cover project-local _opam, BEAM_ROCQ_CMD, and active-PATH coq-lsp discovery
  • keep the fast broker suite Lean-only and document the dedicated Rocq suite

Testing

  • lake build beam-cli beam-daemon beam-client beam-daemon-rocq-smoke-test
  • bash scripts/lint-shell.sh
  • bash tests/test-broker-fast.sh
  • Rocq suite not run locally because coq-lsp is not installed in this workspace PATH

Notes

  • opam-local-packages informs ocaml/setup-ocaml's local pin automation and cache inputs; it does not replace the explicit opam install ... --deps-only step
  • the Rocq runtime now falls back to coq-lsp on PATH after checking project-local _opam roots

@ejgallego
ejgallego merged commit 58f49ae into main Mar 16, 2026
8 checks passed
@ejgallego
ejgallego deleted the codex/rocq-ci-unify-opam branch March 16, 2026 16:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant