chore: switch to rocq lang

contrib/dune

@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name HoTT.Contrib)
  (package coq-hott)
  (theories HoTT))

coq-hott.opam

@@ -30,6 +30,7 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/HoTT/HoTT.git"
+x-maintenance-intent: ["(latest)"]
 depends: [
   "dune" {>= "3.13"}
   ("rocq-core" {>= "9.0"} & "coq-core" {>= "9.0"})

dune

@@ -26,7 +26,8 @@
   (glob_files_rec ./*.vo))
  (action
   (run
-   coqchk
+   rocq
+   check
    -R
    ./theories
    HoTT
@@ -63,21 +64,21 @@
  (action
   (run etc/emacs/run-etags.sh %{vfile})))
 
-; Common flags for Coq
+; Common flags for Rocq
 
 (env
  (dev
-  (coq
-   (coqdoc_flags
+  (rocq
+   (rocqdoc_flags
     :standard
     --interpolate
     --utf8
     --no-externals
     --parse-comments)
    (flags -noinit -indices-matter -color on)))
  (_
-  (coq
-   (coqdoc_flags
+  (rocq
+   (rocqdoc_flags
     :standard
     --interpolate
     --utf8
@@ -116,7 +117,7 @@
      (copy %{file} benched_file.v)
      (run
       %{bin:hyperfine}
-      "%{bin:coqc} -R %{project_root}/theories HoTT -noinit -indices-matter benched_file.v")))
+      "%{bin:rocq} compile -R %{project_root}/theories HoTT -noinit -indices-matter benched_file.v")))
    (echo "Bench finished, report at %{target}:\n\n")
    (cat %{target}))))
 

dune-project

@@ -1,6 +1,6 @@
-(lang dune 3.13)
+(lang dune 3.22)
 
-(using coq 0.8)
+(using rocq 0.12)
 
 (name coq-hott)
 

test/dune

@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name HoTT.Tests)
  (theories HoTT Ltac2))
 

theories/dune

@@ -4,7 +4,7 @@
 
 ; Main theory stanza telling dune how the HoTT library is compiled
 
-(coq.theory
+(rocq.theory
  (name HoTT)
  (package coq-hott)
  (theories Ltac2))