feat: support Rocq 9.0 to 9.2

.github/workflows/ci.yml

@@ -5,9 +5,10 @@ on: [push, pull_request]
 jobs:
   build:
     strategy:
+      fail-fast: false
       matrix:
         runs-on: [ ubuntu-latest ]
-        rocq_version: [ dev ]
+        rocq_version: [ "9.0", "9.1", "9.2", dev ]
     runs-on: ${{ matrix.runs-on }}
 
     steps:

dune-project

@@ -1,9 +1,12 @@
-(lang dune 3.21)
-
-(name mltac2)
+(lang dune 3.17)
 
 (generate_opam_files true)
 
+;; Work-around for Dune 3.17 subst bug: https://github.com/ocaml/dune/issues/11045
+;; LATER: bump to Dune 3.21 once we no longer use Rocq 9.2 in CI
+(subst disabled)
+
+(name mltac2)
 (authors "Dario Halilovic" "Pierre-Marie Pédrot")
 (maintainers "Dario Halilovic")
 (license LGPL-2.1-only)
@@ -17,4 +20,5 @@
  (name mltac2)
  (synopsis "Ltac2 APIs in OCaml")
  (depends
-   rocq-runtime))
+   (coq-core (>= 9.0)) ;; Use coq-core to obtain coqc compatibility binaries
+   ppx_optcomp))

mltac2.opam

@@ -7,12 +7,12 @@ license: "LGPL-2.1-only"
 homepage: "https://github.com/epfl-systemf/mltac2"
 bug-reports: "https://github.com/epfl-systemf/mltac2/issues"
 depends: [
-  "dune" {>= "3.21"}
-  "rocq-runtime"
+  "dune" {>= "3.17"}
+  "coq-core" {>= "9.0"}
+  "ppx_optcomp"
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {dev}
   [
     "dune"
     "build"
@@ -26,4 +26,3 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/epfl-systemf/mltac2.git"
-x-maintenance-intent: ["(latest)"]

src/dune

@@ -1,5 +1,6 @@
 (library
  (name mltac2)
  (public_name mltac2)
- (libraries
-   rocq-runtime.plugins.ltac2))
+ (libraries rocq-runtime.plugins.ltac2)
+ ;; LATER: Replace coq: by rocq: once Dune >= 3.21
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined (%{coq:version.major}, %{coq:version.minor}))")))