WIP: use dune's new rocq plugin

shilangyu · shilangyu · commit 501210c577f3 · 2025-11-28T13:46:17.000+01:00
diff --git a/dune-project b/dune-project
@@ -1,10 +1,10 @@
-(lang dune 3.14)
+(lang dune 3.21)
 
 (name warblre)
 
 (generate_opam_files true)
 
-(using coq 0.8)
+(using rocq 0.11)
 (using melange 0.1)
 (using directory-targets 0.1)
 
@@ -19,8 +19,7 @@
  (synopsis "A mechanization of the specification of ECMAScript regexes")
  (depends
   (ocaml (= 4.14.2))
-  ; LATER: move to rocq-prover once dune plugin is updated: https://github.com/ocaml/dune/pull/12035
-  (coq (>= 9.1.0))))
+  (rocq-prover (>= 9.0.0))))
 
 (package
  (name warblre-engines)
diff --git a/engines/js/dune b/engines/js/dune
@@ -7,7 +7,7 @@
  (files ../common/Extraction.v))
 
 ; Extract with different directives
-(coq.extraction
+(rocq.extraction
  (prelude Extraction)
  (extracted_modules Extracted)
  (theories Warblre Ltac2 Stdlib))
diff --git a/engines/ocaml/dune b/engines/ocaml/dune
@@ -7,7 +7,7 @@
  (files ../common/Extraction.v))
 
 ; Extract with different directives
-(coq.extraction
+(rocq.extraction
  (prelude Extraction)
  (extracted_modules Extracted)
  (theories Warblre Ltac2 Stdlib))
diff --git a/examples/rocq_proof/_CoqProject b/examples/rocq_proof/_CoqProject
diff --git a/mechanization/_CoqProject b/mechanization/_CoqProject
diff --git a/mechanization/dune b/mechanization/dune
@@ -1,6 +1,6 @@
 (include_subdirs qualified)
 
-(coq.theory
+(rocq.theory
  (name Warblre)
  (package warblre)
  (theories Ltac2 Stdlib))
diff --git a/warblre-engines.opam b/warblre-engines.opam
@@ -7,7 +7,7 @@ license: "BSD-3-Clause"
 homepage: "https://github.com/epfl-systemf/warblre"
 bug-reports: "https://github.com/epfl-systemf/warblre/issues"
 depends: [
-  "dune" {>= "3.14"}
+  "dune" {>= "3.21"}
   "warblre" {= version}
   "integers" {>= "0.7.0"}
   "uucp" {>= "15.0.0"}
@@ -30,3 +30,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
+x-maintenance-intent: ["(latest)"]
diff --git a/warblre.opam b/warblre.opam
@@ -7,9 +7,9 @@ license: "BSD-3-Clause"
 homepage: "https://github.com/epfl-systemf/warblre"
 bug-reports: "https://github.com/epfl-systemf/warblre/issues"
 depends: [
-  "dune" {>= "3.14"}
+  "dune" {>= "3.21"}
   "ocaml" {= "4.14.2"}
-  "coq" {>= "9.1.0"}
+  "rocq-prover" {>= "9.0.0"}
   "odoc" {with-doc}
 ]
 build: [
@@ -26,3 +26,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
+x-maintenance-intent: ["(latest)"]

Original file line number	Diff line number	Diff line change
`@@ -7,7 +7,7 @@ license: "BSD-3-Clause"`
`7`	`7`	`homepage: "https://github.com/epfl-systemf/warblre"`
`8`	`8`	`bug-reports: "https://github.com/epfl-systemf/warblre/issues"`
`9`	`9`	`depends: [`
`10`		`- "dune" {>= "3.14"}`
	`10`	`+ "dune" {>= "3.21"}`
`11`	`11`	`"warblre" {= version}`
`12`	`12`	`"integers" {>= "0.7.0"}`
`13`	`13`	`"uucp" {>= "15.0.0"}`
`@@ -30,3 +30,4 @@ build: [`
`30`	`30`	`"@doc" {with-doc}`
`31`	`31`	`]`
`32`	`32`	`]`
	`33`	`+x-maintenance-intent: ["(latest)"]`
Original file line number	Diff line number	Diff line change
`@@ -7,9 +7,9 @@ license: "BSD-3-Clause"`
`7`	`7`	`homepage: "https://github.com/epfl-systemf/warblre"`
`8`	`8`	`bug-reports: "https://github.com/epfl-systemf/warblre/issues"`
`9`	`9`	`depends: [`
`10`		`- "dune" {>= "3.14"}`
	`10`	`+ "dune" {>= "3.21"}`
`11`	`11`	`"ocaml" {= "4.14.2"}`
`12`		`- "coq" {>= "9.1.0"}`
	`12`	`+ "rocq-prover" {>= "9.0.0"}`
`13`	`13`	`"odoc" {with-doc}`
`14`	`14`	`]`
`15`	`15`	`build: [`
`@@ -26,3 +26,4 @@ build: [`
`26`	`26`	`"@doc" {with-doc}`
`27`	`27`	`]`
`28`	`28`	`]`
	`29`	`+x-maintenance-intent: ["(latest)"]`