Add rocq-bignums opam package

.github/workflows/docker-action.yml

@@ -38,9 +38,11 @@ jobs:
               opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev # docker-coq
               opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev # docker-coq
               opam pin add -n -y -k version coq ${{ matrix.coq_version }} # docker-coq
-              opam pin add -n -y -k path $PACKAGE.dev $WORKDIR
+              opam pin add -n -y -k path rocq-bignums.dev $WORKDIR
+              opam pin add -n -y -k path coq-bignums.dev $WORKDIR
               opam update -y
-              opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --ignore-constraints-on=dune
+              opam install --confirm-level=unsafe-yes -j 2 rocq-bignums --ignore-constraints-on=dune
+              opam install --confirm-level=unsafe-yes -j 2 coq-bignums --ignore-constraints-on=dune
             endGroup
           script: |
             startGroup "Post install"

coq-bignums.opam

@@ -10,20 +10,11 @@ dev-repo: "git+https://github.com/coq-community/bignums.git"
 bug-reports: "https://github.com/coq-community/bignums/issues"
 license: "LGPL-2.1-only"
 
-synopsis: "Bignums, the Coq library of arbitrarily large numbers"
-description: """
-This Coq library provides BigN, BigZ, and BigQ that used to
-be part of the standard library."""
+synopsis: "Compatibility wrapper for rocq-bignums"
 
-build: [make "-j%{jobs}%"]
-install: [
-  [make "install"]
-  [make "-C" "tests" "-j%{jobs}%"] {with-test}
-]
 depends: [
-  "ocaml"
-  "rocq-core" {>= "9.0" & < "9.1~"}
-  "rocq-stdlib"
+  "rocq-bignums" {= version}
+  "coq-stdlib"
 ]
 
 tags: [

rocq-bignums.opam

@@ -0,0 +1,42 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+version: "dev"
+
+homepage: "https://github.com/coq-community/bignums"
+dev-repo: "git+https://github.com/coq-community/bignums.git"
+bug-reports: "https://github.com/coq-community/bignums/issues"
+license: "LGPL-2.1-only"
+
+synopsis: "Bignums, the Rocq library of arbitrarily large numbers"
+description: """
+This Rocq library provides BigN, BigZ, and BigQ that used to
+be part of the standard library."""
+
+build: [make "-j%{jobs}%"]
+install: [
+  [make "install"]
+  [make "-C" "tests" "-j%{jobs}%"] {with-test}
+]
+depends: [
+  "ocaml"
+  "rocq-core" {>= "9.0" & < "9.1~"}
+  "rocq-stdlib"
+]
+
+tags: [
+  "category:Miscellaneous/Coq Extensions"
+  "category:Mathematics/Arithmetic and Number Theory/Number theory"
+  "category:Mathematics/Arithmetic and Number Theory/Rational numbers"
+  "keyword:integer numbers"
+  "keyword:rational numbers"
+  "keyword:arithmetic"
+  "keyword:arbitrary precision"
+  "logpath:Bignums"
+]
+authors: [
+  "Laurent Théry"
+  "Benjamin Grégoire"
+  "Arnaud Spiwack"
+  "Evgeny Makarov"
+  "Pierre Letouzey"
+]