From e57bd3da895801887e66dd75b8e8d7a858006025 Mon Sep 17 00:00:00 2001 From: Miriam Polzer Date: Wed, 26 Aug 2026 13:39:49 +0200 Subject: [PATCH 1/3] Support Rocq 9.0 minimum, update CI, opam, and tools Drop support for Coq <= 8.20 and transition the build system and tooling to Rocq 9.0 minimum. - Update Makefile and Makefile.local.common to use rocq, rocq makefile, and rocq top directly. - Decouple version probing from $(COQC) using ROCQ variable so that wrapper commands and compiler overrides do not break $(COQC) top. - Update Makefile.coq-versions-lite to use rocq --version and rocq compile -config, avoiding conflicting .coq-version strings and preventing infinite makefile remake-and-restart loops. - Update CI scripts (describe-system-config.sh, github-actions-make.sh, coq-opam-package.yml) to invoke rocq directly without legacy coq fallbacks. - Add Rocq 9.0, 9.1, and 9.2 to Docker and Opam CI matrices. - Remove legacy `opam install coq` workaround from Docker CI so that preinstalled Rocq 9.x binaries are preserved in the environment. - Update Debian CI package dependencies to coq, libcoq-stdlib, and libcoq-core-ocaml-dev. - Update coq-rewriter.opam bounds to ocaml >= 4.14.0 and coq >= 9.0~. --- .github/workflows/coq-docker.yml | 4 +--- .github/workflows/coq-opam-package.yml | 14 +++++++------- Makefile | 2 +- Makefile.local.common | 14 ++++++++------ coq-rewriter.opam | 4 ++-- etc/ci/describe-system-config.sh | 6 +++--- etc/ci/github-actions-make.sh | 2 +- .../PerfTesting/Makefile.coq-versions-lite | 8 ++++---- 8 files changed, 27 insertions(+), 27 deletions(-) diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 62c5075df..b7bd76a9c 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -17,7 +17,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: [ '8.19', '8.20' , '9.0' , '9.1' ] + coq-version: [ '9.0' , '9.1' , '9.2' ] extra-gh-reportify: [ '' ] skip-validate: [ '' ] include: @@ -49,7 +49,6 @@ jobs: sudo apt-get update -y sudo apt-get install -y python-is-python3 python3 eval $(opam env) - opam install coq -y echo '::endgroup::' echo '::remove-matcher owner=coq-problem-matcher::' CI=1 etc/ci/describe-system-config.sh @@ -78,7 +77,6 @@ jobs: sudo apt-get update -y sudo apt-get install -y python-is-python3 python3 eval $(opam env) - opam install coq -y echo '::endgroup::' echo '::remove-matcher owner=coq-problem-matcher::' etc/ci/github-actions-make.sh TIMED=1 validate COQCHKFLAGS="-o" diff --git a/.github/workflows/coq-opam-package.yml b/.github/workflows/coq-opam-package.yml index f237699f1..dc00d1235 100644 --- a/.github/workflows/coq-opam-package.yml +++ b/.github/workflows/coq-opam-package.yml @@ -17,7 +17,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: ['dev', '8.20.0', '8.19.0', '9.0.0' , '9.1.0' ] + coq-version: ['dev', '9.0.0', '9.1.0', '9.2.0'] os: [{name: 'Ubuntu', runs-on: 'ubuntu-latest', ocaml-compiler: '4.14.0', @@ -127,14 +127,14 @@ jobs: echo ::group::opam list opam list echo ::endgroup:: - echo ::group::coqc --config - opam exec -- coqc --config + echo ::group::rocq --config + opam exec -- rocq --config echo ::endgroup:: - echo ::group::coqc --version - opam exec -- coqc --version + echo ::group::rocq --version + opam exec -- rocq --version echo ::endgroup:: - echo ::group::echo ~ coqtop - echo "" | opam exec -- coqtop + echo ::group::echo ~ rocq top + echo "" | opam exec -- rocq top echo ::endgroup:: - run: opam install coq-rewriter ${{ matrix.os.opam-jobs-flag }} diff --git a/Makefile b/Makefile index 48e7275d2..8fa80daac 100644 --- a/Makefile +++ b/Makefile @@ -81,7 +81,7 @@ endif # We must work around COQBUG(https://github.com/coq/coq/issues/10907) and fix the conf target Makefile.coq Makefile-old.conf: Makefile _CoqProject $(COQ_VERSION_FILE) $(SHOW)'COQ_MAKEFILE -f _CoqProject > Makefile.coq' - $(HIDE)(($(COQBIN)coq_makefile -f _CoqProject -o Makefile-old && cat Makefile-old | sed s'/Makefile-old.conf:/Makefile-old-old.conf:/g' | sed 's/Makefile-old.local/Makefile.local/g; s/^-\?include Makefile.local-late$$//g' $(EXTRA_SED_FOR_DEPS)); echo; echo 'include Makefile.local-late') > Makefile.coq && rm Makefile-old + $(HIDE)(("$(COQBIN)rocq" makefile -f _CoqProject -o Makefile-old && cat Makefile-old | sed s'/Makefile-old.conf:/Makefile-old-old.conf:/g' | sed 's/Makefile-old.local/Makefile.local/g; s/^-\?include Makefile.local-late$$//g' $(EXTRA_SED_FOR_DEPS)); echo; echo 'include Makefile.local-late') > Makefile.coq && rm Makefile-old Makefile.coq: | Makefile-old.conf diff --git a/Makefile.local.common b/Makefile.local.common index 7556c3ac9..5ca8e7b1d 100644 --- a/Makefile.local.common +++ b/Makefile.local.common @@ -18,14 +18,16 @@ TIMECMD_FULL?= TIMER_FULL=$(if $(TIMED), $(STDTIME_FULL), $(TIMECMD_FULL)) COQ_VERSION_FILE = .coq-version -COQ_VERSION_PREFIX = The Coq Proof Assistant, version ROCQ_VERSION_PREFIX = The Rocq Prover, version -COQ_VERSION_COQTOP_CMD := $(COQBIN)coqtop /dev/null) -COQ_VERSION := $(firstword $(subst $(ROCQ_VERSION_PREFIX),,$(subst $(COQ_VERSION_PREFIX),,$(COQC_VERSION_FULL)))) +COQ_VERSION_PREFIX = The Coq Proof Assistant, version +ROCQ ?= "$(COQBIN)rocq" +COQ_VERSION_COQTOP_CMD := $(ROCQ) top /dev/null) +COQC_VERSION_FULL := $(ROCQ_VERSION_FULL) +COQ_VERSION := $(firstword $(subst $(ROCQ_VERSION_PREFIX),,$(subst $(COQ_VERSION_PREFIX),,$(ROCQ_VERSION_FULL)))) -COQ_EXTENDED_VERSION:=$(strip $(shell $(COQ_VERSION_COQTOP_CMD) 2>/dev/null) $(COQC_VERSION_FULL)) +COQ_EXTENDED_VERSION:=$(strip $(shell $(COQ_VERSION_COQTOP_CMD) 2>/dev/null) $(ROCQ_VERSION_FULL)) COQ_EXTENDED_VERSION_OLD:=$(strip $(shell cat $(COQ_VERSION_FILE) 2>/dev/null)) # Extract "major.minor" robustly from version strings like "9.2", "9.2.0", diff --git a/coq-rewriter.opam b/coq-rewriter.opam index a8496545b..c124f82bf 100644 --- a/coq-rewriter.opam +++ b/coq-rewriter.opam @@ -15,8 +15,8 @@ build: [ install: [make "install"] depends: [ "conf-findutils" {build} - "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")} - "coq" {>= "8.19~"} + "ocaml" {build & >= "4.14.0"} + "coq" {>= "9.0~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography" diff --git a/etc/ci/describe-system-config.sh b/etc/ci/describe-system-config.sh index 0bfad6121..1918b29c2 100755 --- a/etc/ci/describe-system-config.sh +++ b/etc/ci/describe-system-config.sh @@ -53,9 +53,9 @@ group ocamlfind query rocq-runtime group ocamlfind query rocq-runtime.plugins group ocamlfind query rocq-runtime.plugins.ltac group "ocamlfind query coq | xargs find" -group coqc --config -group coqc --version -group "true | coqtop" +group rocq --config +group rocq --version +group "true | rocq top" group etc/machine.sh group "echo PATH=$PATH" group "echo SHELL=$SHELL" diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh index 20526d297..d4c3fa70d 100755 --- a/etc/ci/github-actions-make.sh +++ b/etc/ci/github-actions-make.sh @@ -20,7 +20,7 @@ if [ "$1" == "--warnings" ]; then shift fi if [ ! -z "${reportify}" ]; then - reportify="COQC='$(pwd)/etc/coq-scripts/github/reportify-coq.sh'${reportify} ${COQBIN}coqc" + reportify="COQC='$(pwd)/etc/coq-scripts/github/reportify-coq.sh'${reportify} ${COQBIN}rocq compile" fi rm -f finished.ok diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite b/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite index 5f443c321..97cbe842f 100644 --- a/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite +++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite @@ -10,10 +10,10 @@ COQ_VERSION_SHORT_DATE_FILE = .coq-version-short-date COQ_VERSION_CONFIG_FILE := .coq-version-config COQ_VERSION_OCAML_VERSION_FILE := .coq-version-ocaml-version COQ_VERSION_OCAML_CONFIG_FILE := .coq-version-ocaml-config -COQ_VERSION_PREFIX = The Coq Proof Assistant, version -COQ_VERSION_FULL := $(subst $(COQ_VERSION_PREFIX),,$(shell $(COQBIN)coqc --version 2>/dev/null)) +COQ_VERSION_PREFIX = The Rocq Prover, version +COQ_VERSION_FULL := $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)rocq" --version 2>/dev/null)) COQ_VERSION := $(firstword $(COQ_VERSION_FULL)) -COQ_VERSION_CONFIG_CMD = $(COQBIN)coqc -config 2>/dev/null +COQ_VERSION_CONFIG_CMD = "$(COQBIN)rocq" compile -config 2>/dev/null COQ_VERSION_DATE := $(subst $(OPEN_PAREN),,$(subst $(CLOSE_PAREN),,$(wordlist 2, 3, $(COQ_VERSION_FULL)))) COQ_VERSION_COMPILATION := $(subst $(JOINER)with,$(SPACE)with,$(subst $(SPACE),$(JOINER),$(wordlist 4, $(words $(COQ_VERSION_FULL)),$(COQ_VERSION_FULL)))) COQ_VERSION_COMPILATION_DATE := $(subst $(JOINER),$(SPACE),$(subst compiled$(JOINER)on$(JOINER),,$(firstword $(COQ_VERSION_COMPILATION)))) @@ -23,7 +23,7 @@ VERSION_FILES := $(COQ_VERSION_FILE) $(COQ_VERSION_SHORT_FILE) $(COQ_VERSION_SHO MACHINE_FILE = .machine MACHINE_EXTENDED_FILE = .machine-extended -COQ_EXTENDED_VERSION := $(shell (true | $(COQBIN)coqtop 2>/dev/null; $(COQBIN)coqc --version 2>/dev/null)) +COQ_EXTENDED_VERSION := $(shell (true | "$(COQBIN)rocq" top 2>/dev/null; "$(COQBIN)rocq" --version 2>/dev/null)) COQ_EXTENDED_VERSION_OLD := $(shell cat $(COQ_VERSION_FILE) 2>/dev/null) HAS_LTAC2:= From 856442631e67265f0ab56e1043960681e8319f47 Mon Sep 17 00:00:00 2001 From: Lukas Zobernig Date: Wed, 2 Sep 2026 14:25:12 +0000 Subject: [PATCH 2/3] Transition opam dependencies directly to rocq package names --- coq-rewriter.opam | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/coq-rewriter.opam b/coq-rewriter.opam index c124f82bf..6ed78cd19 100644 --- a/coq-rewriter.opam +++ b/coq-rewriter.opam @@ -15,8 +15,9 @@ build: [ install: [make "install"] depends: [ "conf-findutils" {build} - "ocaml" {build & >= "4.14.0"} - "coq" {>= "9.0~"} + "ocaml" + "rocq-core" {>= "9.0~"} + "rocq-stdlib" {>= "9.0~"} ] dev-repo: "git+https://github.com/mit-plv/rewriter.git" synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography" From 77decdf492e84ac27b1756bfcf829933feb99622 Mon Sep 17 00:00:00 2001 From: Lukas Zobernig Date: Thu, 3 Sep 2026 11:05:45 +0000 Subject: [PATCH 3/3] Avoid cross-PR CI cancellation by scoping concurrency to PR number --- .github/workflows/coq-alpine.yml | 2 +- .github/workflows/coq-debian.yml | 2 +- .github/workflows/coq-docker.yml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml index e38e3a2d6..79b265efc 100644 --- a/.github/workflows/coq-alpine.yml +++ b/.github/workflows/coq-alpine.yml @@ -25,7 +25,7 @@ jobs: name: alpine-${{ matrix.alpine }} concurrency: - group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }} + group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.event.pull_request.number || github.head_ref || github.run_id }} cancel-in-progress: true steps: diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml index 85115eee9..8330bdd2a 100644 --- a/.github/workflows/coq-debian.yml +++ b/.github/workflows/coq-debian.yml @@ -25,7 +25,7 @@ jobs: container: debian:${{ matrix.debian }} concurrency: - group: ${{ github.workflow }}-debian-${{ matrix.debian }}-${{ github.head_ref || github.run_id }} + group: ${{ github.workflow }}-debian-${{ matrix.debian }}-${{ github.event.pull_request.number || github.head_ref || github.run_id }} cancel-in-progress: true steps: diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 7e69ba069..89d3ccc69 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -29,7 +29,7 @@ jobs: name: ${{ matrix.coq-version }} concurrency: - group: ${{ github.workflow }}-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} + group: ${{ github.workflow }}-${{ matrix.coq-version }}-${{ github.event.pull_request.number || github.head_ref || github.run_id }} cancel-in-progress: true steps: