From b2c53f922e109cf905556c3fe5b71fe76f36277c Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 3 Jul 2026 20:15:45 +0100 Subject: [PATCH 1/6] Fix Dune Rocq msg --- coq/Cerberus/dune | 2 +- coq/Cn/dune | 2 +- coq/Reasoning/dune | 2 +- dune-project | 4 ++-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/coq/Cerberus/dune b/coq/Cerberus/dune index da7c180a4..699f6b15a 100644 --- a/coq/Cerberus/dune +++ b/coq/Cerberus/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name Cerberus) (package cn-coq) (synopsis "Coq formalization of some Cerberus types") diff --git a/coq/Cn/dune b/coq/Cn/dune index 94123c240..af7310094 100644 --- a/coq/Cn/dune +++ b/coq/Cn/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name Cn) (package cn-coq) (synopsis "Coq formalization of CN") diff --git a/coq/Reasoning/dune b/coq/Reasoning/dune index a1468eb50..66b7b08df 100644 --- a/coq/Reasoning/dune +++ b/coq/Reasoning/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name Reasoning) (package cn-coq) (synopsis "CN Reasoning in Coq") diff --git a/dune-project b/dune-project index 273e6abb6..4e19a19f6 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 3.8) +(lang dune 3.21) (name cn) -(using coq 0.8) +(using rocq 0.11) From 2633415f2cb15c9029bf5d6848dacdd26e2aa3f0 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 3 Jul 2026 20:29:45 +0100 Subject: [PATCH 2/6] Fix Rocq CI --- .github/workflows/rocq.yml | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 46102bfe5..6080068e2 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -41,16 +41,16 @@ jobs: uses: actions/cache/restore@v5 with: path: ~/.opam - key: ${{ matrix.version }}-with-coq-${{ hashFiles('cn.opam') }} + key: ${{ matrix.version }}-with-rocq-${{ hashFiles('cn.opam') }} - name: Setup OPAM if: steps.cache-opam-restore.outputs.cache-hit != 'true' run: | opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }} - opam switch create ${{ matrix.version }}-with-coq ${{ matrix.version }} - eval $(opam env --switch=${{ matrix.version }}-with-coq) - opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released - opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git + opam switch create ${{ matrix.version }}-with-rocq ${{ matrix.version }} + eval $(opam env --switch=${{ matrix.version }}-with-rocq) + opam repo add --yes --this-switch rocq-released https://rocq.inria.fr/opam/released + opam pin --yes -n rocq-struct-tact https://github.com/uwplse/StructTact.git opam install --deps-only --yes ./cn.opam - name: Save OPAM cache @@ -58,18 +58,18 @@ jobs: if: steps.cache-opam-restore.outputs.cache-hit != 'true' with: path: ~/.opam - key: ${{ matrix.version }}-with-coq-${{ hashFiles('cn.opam') }} + key: ${{ matrix.version }}-with-rocq-${{ hashFiles('cn.opam') }} - - name: Install CN (with Coq) + - name: Install CN (with rocq) run: | - opam switch ${{ matrix.version }}-with-coq - eval $(opam env --switch=${{ matrix.version }}-with-coq ) + opam switch ${{ matrix.version }}-with-rocq + eval $(opam env --switch=${{ matrix.version }}-with-rocq ) opam pin --yes --no-action add cn . - opam pin --yes --no-action add cn-coq . - opam install --yes cn cn-coq + opam pin --yes --no-action add cn-rocq . + opam install --yes cn cn-rocq - - name: Run CN-Coq tests + - name: Run CN-rocq tests run: | - opam switch ${{ matrix.version }}-with-coq - eval $(opam env --switch=${{ matrix.version }}-with-coq ) - ./tests/diff-prog.py tests/run-cn-coq.sh tests/cn/coq.json --max-workers=2 2> diff.patch || (cat diff.patch; exit 1) + opam switch ${{ matrix.version }}-with-rocq + eval $(opam env --switch=${{ matrix.version }}-with-rocq ) + ./tests/diff-prog.py tests/run-cn-rocq.sh tests/cn/rocq.json --max-workers=2 2> diff.patch || (cat diff.patch; exit 1) From 4c0dc51d007377bd66411fe23771d1dcb5427680 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 3 Jul 2026 20:39:10 +0100 Subject: [PATCH 3/6] Fix Rocq CI: revert over-eager coq->rocq renamings The previous CI fix renamed every "coq" token to "rocq", but several of those name external resources that were not renamed upstream, so the workflow would fail at each step: - opam repo URL: rocq.inria.fr does not resolve; the released archive is still served from coq.inria.fr/opam/released. - coq-struct-tact is still the published package name (uwplse/StructTact ships coq-struct-tact.opam); there is no rocq-struct-tact. - The package file is cn-coq.opam, so pin/install must use cn-coq. - The test driver and data files are tests/run-cn-coq.sh and tests/cn/coq.json; the rocq-named variants do not exist. Keep the purely internal labels (cache keys, switch names, step titles) as rocq. The build-system rename (dune's coq->rocq extension) is unaffected and stays. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/rocq.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 6080068e2..532a7c7d0 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -49,8 +49,8 @@ jobs: opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }} opam switch create ${{ matrix.version }}-with-rocq ${{ matrix.version }} eval $(opam env --switch=${{ matrix.version }}-with-rocq) - opam repo add --yes --this-switch rocq-released https://rocq.inria.fr/opam/released - opam pin --yes -n rocq-struct-tact https://github.com/uwplse/StructTact.git + opam repo add --yes --this-switch rocq-released https://coq.inria.fr/opam/released + opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git opam install --deps-only --yes ./cn.opam - name: Save OPAM cache @@ -65,11 +65,11 @@ jobs: opam switch ${{ matrix.version }}-with-rocq eval $(opam env --switch=${{ matrix.version }}-with-rocq ) opam pin --yes --no-action add cn . - opam pin --yes --no-action add cn-rocq . - opam install --yes cn cn-rocq + opam pin --yes --no-action add cn-coq . + opam install --yes cn cn-coq - name: Run CN-rocq tests run: | opam switch ${{ matrix.version }}-with-rocq eval $(opam env --switch=${{ matrix.version }}-with-rocq ) - ./tests/diff-prog.py tests/run-cn-rocq.sh tests/cn/rocq.json --max-workers=2 2> diff.patch || (cat diff.patch; exit 1) + ./tests/diff-prog.py tests/run-cn-coq.sh tests/cn/coq.json --max-workers=2 2> diff.patch || (cat diff.patch; exit 1) From 8f0abf7f9ca0eb2413a12afa1ad77dada50e1c82 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 3 Jul 2026 20:59:35 +0100 Subject: [PATCH 4/6] Fix Rocq CI --- cn-coq.opam | 1 + 1 file changed, 1 insertion(+) diff --git a/cn-coq.opam b/cn-coq.opam index 9e414dafa..2d2134a02 100644 --- a/cn-coq.opam +++ b/cn-coq.opam @@ -18,6 +18,7 @@ depends: [ "coq" {= "8.20.1"} "coq-ext-lib" "coq-struct-tact" + "dune" {= "3.21"} ] build: [ ["dune" "subst"] {pinned} From 6b96c1ed22e2a868a836e594bcc109812659be46 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 3 Jul 2026 21:03:10 +0100 Subject: [PATCH 5/6] Fix Rocq CI --- .github/workflows/rocq.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 532a7c7d0..6ce4f0087 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -51,7 +51,7 @@ jobs: eval $(opam env --switch=${{ matrix.version }}-with-rocq) opam repo add --yes --this-switch rocq-released https://coq.inria.fr/opam/released opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git - opam install --deps-only --yes ./cn.opam + opam install --deps-only --yes ./cn.opam ./cn-coq.opam - name: Save OPAM cache uses: actions/cache/save@v5 From bae7f6643d54b08bb0a902b935f7851f083a2689 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 3 Jul 2026 21:20:09 +0100 Subject: [PATCH 6/6] Fix Rocq CI --- cn-coq.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cn-coq.opam b/cn-coq.opam index 2d2134a02..02e65861c 100644 --- a/cn-coq.opam +++ b/cn-coq.opam @@ -18,7 +18,7 @@ depends: [ "coq" {= "8.20.1"} "coq-ext-lib" "coq-struct-tact" - "dune" {= "3.21"} + "dune" {= "3.21.1"} ] build: [ ["dune" "subst"] {pinned}