setup-rocq-test

Integration tests for setup-rocq.

setup-rocq's own CI can only check that the action runs without erroring. The things most likely to break are the ones a single job cannot see: whether the cache actually round-trips, whether a restored switch has the compiler that was asked for, and whether the environment the action exports reaches later steps. Those need a real project, more than one job, and more than one run — which is what lives here.

Layout

Path	What it is
smoke/	A standalone .v file that requires nothing outside the prelude
stdlib/	A project that Requires the standard library
theories/	A dune project using the rocq extension
makefile-project/	A _CoqProject built via rocq makefile / coq_makefile
pinned/	An opam file with Rocq pin-depends, for the pinned-install path
scripts/	The assertion library, the verifier, and the builders

smoke/, theories/, and makefile-project/ deliberately contain no Require, so one source file works across every version in the matrix including dev and weekly.

stdlib/ is the opposite on purpose. It Requires List, Arith, Lia, String, and Bool, which is the only sample here that would notice if rocq-stdlib were missing or unfindable — a switch with rocq-core alone builds everything else fine and fails that one. It targets Rocq 9.2+, since the stdlib's root namespace was renamed from Coq to Stdlib in Rocq 9.

Version policy

The matrix targets Rocq 9.2 and later. Older releases are not a priority: supporting 8.x would mean a second copy of every sample that touches the standard library, to cover a line nobody here is on. dev and weekly build only the Require-free sample, because master can move ahead of both the dune rocq extension and the stdlib layout this project pins.

Workflows

Workflow	Trigger	What it proves
lint.yml	every push	The harness itself works: assertions fail when they should
integration.yml	push, PR, weekly, manual	Each rocq-version and platform installs and builds
cache.yml	push to main, weekly, manual	The cache round-trips, and the key separates OCaml versions
cache-on-failure.yml	weekly, manual	A failed build still saves its cache
pinned.yml	weekly, manual	pin-depends overrides rocq-version

case.yml is a reusable workflow holding one parameterised case; the others call it.

Integration jobs install Rocq for real and take tens of minutes, which is why only lint.yml runs on every push.

Testing a branch of the action

uses: does not accept expressions, so the workflows check the action out into .setup-rocq/ and reference it as uses: ./.setup-rocq. That makes the ref a parameter:

gh workflow run integration.yml -f setup-rocq-ref=my-branch
gh workflow run cache.yml -f setup-rocq-ref=my-branch

Use -f setup-rocq-repository=someone/setup-rocq to test a fork. Both default to tchajed/setup-rocq@main.

Because the action is consumed from a checkout, the branch under test must have an up-to-date dist/ committed — the same requirement setup-rocq's own check-dist workflow enforces.

How the cache tests get a deterministic result

This is subtler than it looks, and the first two attempts here were both wrong in the same way.

The obvious approach is to make the cache key unique per run — the jobs call scripts/unique-opam.sh to write an opam file containing the current run_id and point cache-key-opam-files at it — and then assert cache-hit: false on the first job and true on the second.

That does not work. setup-rocq restores with two fallback prefixes in addition to the exact key, and those prefixes do not include the opam-file hash at all:

setup-rocq-v4-<platform>-<arch>-ocaml-<ver>-opam-<series>-rocq-<ver>-<hash>  exact
setup-rocq-v4-<platform>-<arch>-ocaml-<ver>-opam-<series>-rocq-<ver>-        fallback
setup-rocq-v4-<platform>-<arch>-ocaml-<ver>-opam-<series>-                   fallback

So a "cold" job routinely restores an older, compatible archive from a previous run. That is the whole point of the fallbacks — a warm start beats a cold one — and no amount of key seeding will make cache-hit: false true.

The question that is deterministic is whether the key that matched is the one this run computed. That is what the jobs assert, via cache-primary-key and cache-matched-key:

• cold must not have found its own key — nothing has saved it yet. It may well restore something else.
• warm must have found exactly its own key. A fallback match would mean the cold job's save never landed, which is the failure this workflow exists to catch.
• different-ocaml asks for the same Rocq on a different compiler, and its restored key must not contain the cold job's compiler. When the compiler was not part of the key, this job matched the cold archive through the platform-only fallback, skipped switch creation because a cache had been restored, and silently ran on the wrong compiler.

cache-on-failure.yml uses the same exact-hit assertion: a fallback match would pass even if the post step had skipped the save entirely.

All of these pass save-if: true, so the round trip does not depend on which event triggered the workflow — under the default auto, a pull_request run restores but never saves.

Running the checks locally

Everything except the action itself runs without GitHub:

bash scripts/selftest.sh        # test the assertion helpers
shellcheck scripts/*.sh
bash scripts/build.sh all       # needs a Rocq 9.2+ switch on PATH
bash scripts/verify.sh          # needs a switch; expectations come from env

verify.sh reads its expectations from the environment (EXPECT_ROCQ_VERSION, EXPECT_BINARY_VERSION, EXPECT_OCAML_VERSION, EXPECT_CACHE_HIT) and the action's reported outputs from OUT_*. Anything left unset is not checked.

Maintenance

pinned/rocq-pinned-test.opam pins the V9.2.0 release tags of the rocq and stdlib repositories. They are tags rather than a branch so that "did the pin take effect?" has an answer; bump them when the pinned release gets old.