Merge pull request #98 from coq-community/rocq-bignums

Add rocq-bignums opam package

Author: proux01

.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:

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"
 ]
 

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" {= "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"
+]

tests/Makefile

@@ -1,4 +1,4 @@
-COQC=coqc
+ROCQC=rocq c
 
 all: success output
 
@@ -7,10 +7,10 @@ success: $(addsuffix o,$(wildcard success/*.v))
 output: $(addsuffix o,$(wildcard output/*.v))
 
 success/%.vo: success/%.v
-	$(COQC) $<
+	$(ROCQC) $<
 
 output/%.vo: output/%.v
 	input=$<; \
 	output=$${input%.v}.out.real; \
-	$(COQC) $< 2>&1 > $$output; \
+	$(ROCQC) $< 2>&1 > $$output; \
 	diff --strip-trailing-cr $${input%.v}.out $$output