From 7433022e8d179a53d28310d32ba4f1dbbfd602ee Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sat, 25 Jan 2025 11:36:45 +0100
Subject: [PATCH] Add rocq-bignums opam package

---
 .github/workflows/docker-action.yml | 12 ++++++---
 coq-bignums.opam                    | 13 ++-------
 rocq-bignums.opam                   | 42 +++++++++++++++++++++++++++++
 3 files changed, 53 insertions(+), 14 deletions(-)
 create mode 100644 rocq-bignums.opam

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 57afd5c..8761b13 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -32,15 +32,21 @@ jobs:
           opam_file: 'coq-bignums.opam'
           custom_image: ${{ matrix.image }}
           install: |
-            startGroup "Install coq and dependencies"
+            startGroup "Install"
               sudo apt-get update -y -q
               opam remove -y coq-bignums || true # remove coq-bignums if ever in image
               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 --deps-only
+              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"
+              opam list
             endGroup
           export: 'OPAMWITHTEST'
         env:
diff --git a/coq-bignums.opam b/coq-bignums.opam
index 9a9549b..7de0246 100644
--- a/coq-bignums.opam
+++ b/coq-bignums.opam
@@ -7,19 +7,10 @@ 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" {= "dev"}
+  "rocq-bignums" {= version}
   "coq-stdlib"
 ]
 
diff --git a/rocq-bignums.opam b/rocq-bignums.opam
new file mode 100644
index 0000000..246b741
--- /dev/null
+++ b/rocq-bignums.opam
@@ -0,0 +1,42 @@
+opam-version: "2.0"
+maintainer: "pierre.roux@onera.fr"
+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" {= "dev"}
+  "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"
+]