Skip to content

Fix Dune Rocq msg #576

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dc-mak wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Fix Dune Rocq msg #576

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b2c53f9
Fix Dune Rocq msg
dc-mak Jul 3, 2026
2633415
Fix Rocq CI
dc-mak Jul 3, 2026
4c0dc51
Fix Rocq CI: revert over-eager coq->rocq renamings
dc-mak Jul 3, 2026
8f0abf7
Fix Rocq CI
dc-mak Jul 3, 2026
6b96c1e
Fix Rocq CI
dc-mak Jul 3, 2026
bae7f66
Fix Rocq CI
dc-mak Jul 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions .github/workflows/rocq.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,35 +41,35 @@ 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 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://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
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

- 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 )
opam switch ${{ matrix.version }}-with-rocq
eval $(opam env --switch=${{ matrix.version }}-with-rocq )
./tests/diff-prog.py tests/run-cn-coq.sh tests/cn/coq.json --max-workers=2 2> diff.patch || (cat diff.patch; exit 1)
1 change: 1 addition & 0 deletions cn-coq.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ depends: [
"coq" {= "8.20.1"}
"coq-ext-lib"
"coq-struct-tact"
"dune" {= "3.21.1"}
]
build: [
["dune" "subst"] {pinned}
Expand Down
2 changes: 1 addition & 1 deletion coq/Cerberus/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(coq.theory
(rocq.theory
(name Cerberus)
(package cn-coq)
(synopsis "Coq formalization of some Cerberus types")
Expand Down
2 changes: 1 addition & 1 deletion coq/Cn/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(coq.theory
(rocq.theory
(name Cn)
(package cn-coq)
(synopsis "Coq formalization of CN")
Expand Down
2 changes: 1 addition & 1 deletion coq/Reasoning/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(coq.theory
(rocq.theory
(name Reasoning)
(package cn-coq)
(synopsis "CN Reasoning in Coq")
Expand Down
4 changes: 2 additions & 2 deletions dune-project
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(lang dune 3.8)
(lang dune 3.21)
(name cn)

(using coq 0.8)
(using rocq 0.11)
Loading