Merge PR coq#19980: Rename coq-native -> rocq-native

Reviewed-by: ppedrot
Ack-by: SkySkimmer
Co-authored-by: ppedrot <[email protected]>

.gitlab-ci.yml

@@ -41,7 +41,7 @@ variables:
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
   BASE_CACHEKEY: "old_ubuntu_lts-V2024-10-11-f72b1aa7c6"
-  EDGE_CACHEKEY: "edge_ubuntu-V2024-12-13-5c140221f4"
+  EDGE_CACHEKEY: "edge_ubuntu-V2025-01-03-c1da705cbe"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 
@@ -239,16 +239,16 @@ before_script:
   extends: .auto-use-tags
   # OPAM will build out-of-tree so no point in importing artifacts
   script:
-    - if [ "$COQ_CI_NATIVE" = true ]; then opam install -y coq-native; fi
+    - if [ "$ROCQ_CI_NATIVE" = true ]; then opam install -y rocq-native; fi
     - opam pin add --kind=path rocq-runtime.dev .
     - opam pin add --kind=path rocq-core.dev .
     - opam pin add --kind=path coq-stdlib.dev stdlib/
     - if command -v coqc; then exit 1; fi # coq-core didn't get autoinstalled
     - opam pin add --kind=path coqide-server.dev .
     - opam pin add --kind=path coqide.dev .
-    - if [ "$COQ_CI_NATIVE" = true ]; then echo "Definition f x := x + x." > test_native.v; fi
-    - if [ "$COQ_CI_NATIVE" = true ]; then rocq c test_native.v; fi
-    - if [ "$COQ_CI_NATIVE" = true ]; then test -f .coq-native/Ntest_native.cmxs; fi
+    - if [ "$ROCQ_CI_NATIVE" = true ]; then echo "Definition f x := x + x." > test_native.v; fi
+    - if [ "$ROCQ_CI_NATIVE" = true ]; then rocq c test_native.v; fi
+    - if [ "$ROCQ_CI_NATIVE" = true ]; then test -f .coq-native/Ntest_native.cmxs; fi
     - opam pin add --kind=path coq-core.dev .
   after_script:
     - eval $(opam env)
@@ -390,7 +390,7 @@ lint:
 pkg:opam:native:
   extends: .pkg:opam-template
   variables:
-    COQ_CI_NATIVE: "true"
+    ROCQ_CI_NATIVE: "true"
 
 # broken, see eg https://gitlab.com/coq/coq/-/jobs/1754045983
 # pkg:nix:deploy:

coq.opam

@@ -39,7 +39,7 @@ build: [
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+    "-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
   ] {with-test}
   [
     "dune"

coq.opam.template

@@ -4,7 +4,7 @@ build: [
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+    "-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
   ] {with-test}
   [
     "dune"

dev/bench/bench.sh

@@ -424,7 +424,7 @@ create_opam() {
 
     echo "$1_coq_commit_long = $COQ_HASH_LONG"
 
-    if [ ! -z "$coq_native" ]; then opam install coq-native; fi
+    if [ ! -z "$coq_native" ]; then opam install coq-native rocq-native; fi
 
 }
 

dev/ci/docker/edge_ubuntu/Dockerfile

@@ -59,7 +59,7 @@ ENV COMPILER="4.14.1" \
 # `ci-template-flambda` with everything.
 RUN opam init -a --disable-sandboxing --bare && eval $(opam env) && opam update && \
     opam switch create "${COMPILER}+flambda" \
-      --repositories default,ocaml-beta=git+https://github.com/ocaml/ocaml-beta-repository.git \
+      --repositories default,ocaml-beta=git+https://github.com/ocaml/ocaml-beta-repository.git,coq-core-dev=https://coq.inria.fr/opam/core-dev \
       --packages="ocaml-variants.${COMPILER}+options,ocaml-option-flambda" && eval $(opam env) && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM $CI_OPAM_EDGE && \
     opam clean -a -c

dune-project

@@ -30,7 +30,7 @@
   (ocamlfind (>= 1.8.1))
   (zarith (>= 1.11))
   (conf-linux-libc-dev (= :os "linux")))
- (depopts coq-native memprof-limits memtrace)
+ (depopts rocq-native memprof-limits memtrace)
  (synopsis "The Coq Proof Assistant -- Core Binaries and Tools")
  (description "Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -60,7 +60,7 @@ prelude, now living in the rocq-core package."))
  (name rocq-core)
  (depends
   (rocq-runtime (= :version)))
- (depopts coq-native)
+ (depopts rocq-native)
  (synopsis "The Coq Proof Assistant with its prelude")
  (description "Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable

rocq-core.opam

@@ -28,7 +28,7 @@ depends: [
   "rocq-runtime" {= version}
   "odoc" {with-doc}
 ]
-depopts: ["coq-native"]
+depopts: ["rocq-native"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}

rocq-runtime.opam

@@ -34,15 +34,15 @@ depends: [
   "conf-linux-libc-dev" {os = "linux"}
   "odoc" {with-doc}
 ]
-depopts: ["coq-native" "memprof-limits" "memtrace"]
+depopts: ["rocq-native" "memprof-limits" "memtrace"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}
   [ "./configure"
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+    "-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
   ]
   [
     "dune"

rocq-runtime.opam.template

@@ -4,7 +4,7 @@ build: [
     "-prefix" prefix
     "-mandir" man
     "-libdir" "%{lib}%/coq"
-    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+    "-native-compiler" "yes" {rocq-native:installed} "no" {!rocq-native:installed}
   ]
   [
     "dune"

stdlib/coq-stdlib.opam

@@ -28,7 +28,7 @@ depends: [
   "rocq-core" {= version}
   "odoc" {with-doc}
 ]
-depopts: ["coq-native"]
+depopts: ["rocq-native"]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}

stdlib/dune-project

@@ -25,7 +25,7 @@
  (depends
   rocq-runtime
   (rocq-core (= :version)))
- (depopts coq-native)
+ (depopts rocq-native)
  (synopsis "The Coq Proof Assistant -- Standard Library")
  (description "Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable