Compile without coq shims

Author: proux01

.github/workflows/coq-action.yml

@@ -15,15 +15,15 @@ jobs:
     strategy:
       matrix:
         image:
-          - mathcomp/mathcomp:2.6.0-coq-9.0
-          - mathcomp/mathcomp:2.6.0-coq-9.1
-          - mathcomp/mathcomp:2.6.0-coq-9.2
+          - mathcomp/mathcomp:2.6.0-rocq-prover-9.0
+          - mathcomp/mathcomp:2.6.0-rocq-prover-9.1
+          - mathcomp/mathcomp:2.6.0-rocq-prover-9.2
       fail-fast: false
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1
       with:
-        opam_file: 'coq-mathcomp-dioid.opam'
+        opam_file: 'rocq-mathcomp-dioid.opam'
         custom_image: ${{ matrix.image }}
         custom_script: |
           startGroup Print opam config
@@ -33,18 +33,18 @@ jobs:
           startGroup Update opam cache
             opam update -y
           endGroup
-          startGroup Build coq-mathcomp-dioid dependencies
-            opam pin add -n -y -k path coq-mathcomp-dioid .
-            opam remove coq-mathcomp-character coq-mathcomp-field coq-mathcomp-solvable # coq-mathcomp-algebra is enough
-            opam install -y -j ${NJOBS} coq-mathcomp-dioid --deps-only
+          startGroup Build rocq-mathcomp-dioid dependencies
+            opam pin add -n -y -k path rocq-mathcomp-dioid .
+            opam remove -y rocq-mathcomp-character rocq-mathcomp-field rocq-mathcomp-solvable # rocq-mathcomp-algebra is enough
+            opam install -y -j ${NJOBS} rocq-mathcomp-dioid --deps-only
             opam list
           endGroup
-          startGroup Build coq-mathcomp-dioid
-            opam install -y -v -j ${NJOBS} coq-mathcomp-dioid
+          startGroup Build rocq-mathcomp-dioid
+            opam install -y -v -j ${NJOBS} rocq-mathcomp-dioid
             opam list
           endGroup
           startGroup Uninstallation test
-            opam remove -y coq-mathcomp-dioid
+            opam remove -y rocq-mathcomp-dioid
           endGroup
 
 # See also:

.gitignore

@@ -1,7 +1,7 @@
 *~
-Makefile.coq
-Makefile.coq.conf
-.Makefile.coq.d
+Makefile.rocq
+Makefile.rocq.conf
+.Makefile.rocq.d
 .*.aux
 *.glob
 *.vo

Makefile

@@ -1,33 +1,33 @@
 # Makefile for dioid
 
 COQ_PROJ := _CoqProject
-COQ_MAKEFILE := Makefile.coq
-COQ_MAKE := +$(MAKE) -f $(COQ_MAKEFILE)
+ROCQ_MAKEFILE := Makefile.rocq
+ROCQ_MAKE := +$(MAKE) -f $(ROCQ_MAKEFILE)
 
-ifneq "$(COQBIN)" ""
-	COQBIN := $(COQBIN)/
+ifneq "$(ROCQBIN)" ""
+	ROCQBIN := $(ROCQBIN)/
 else
-	COQBIN := $(dir $(shell which coqc))
+	ROCQBIN := $(dir $(shell which coqc))
 endif
-export COQBIN
+export ROCQBIN
 
-all install html gallinahtml: $(COQ_MAKEFILE) Makefile
-	$(COQ_MAKE) $@
+all install html gallinahtml: $(ROCQ_MAKEFILE) Makefile
+	$(ROCQ_MAKE) $@
 
 %.vo: %.v
-	$(COQ_MAKE) $@
+	$(ROCQ_MAKE) $@
 
-$(COQ_MAKEFILE): $(COQ_PROJ)
-	$(COQBIN)coq_makefile -f $< -o $@
+$(ROCQ_MAKEFILE): $(COQ_PROJ)
+	$(ROCQBIN)rocq makefile -f $< -o $@
 
 clean:
-	-$(COQ_MAKE) clean
+	-$(ROCQ_MAKE) clean
 
 distclean: clean
-	$(RM) $(COQ_MAKEFILE) $(COQ_MAKEFILE).conf
+	$(RM) $(ROCQ_MAKEFILE) $(ROCQ_MAKEFILE).conf
 	$(RM) *~ .*.aux .lia.cache
 
 
--include $(COQ_MAKEFILE).conf
+-include $(ROCQ_MAKEFILE).conf
 
 .PHONY: all install html gallinahtml clean distclean

coq-mathcomp-dioid.opam

@@ -9,43 +9,8 @@ dev-repo: "git+https://github.com/math-comp/dioid.git"
 bug-reports: "https://github.com/math-comp/dioid/issues"
 license: "CECILL-B"
 
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [make "install"]
-
 depends: [
-  "coq-core" { >= "9.0" }
-  "rocq-mathcomp-algebra" { >= "2.6" }
-  "rocq-mathcomp-classical" { >= "1.8" }
-]
-synopsis: "Dioid"
-description: """
-Definitions of the algebraic structure of dioid following the style of
-ssralg in the Mathcomp library.
-
-The main algebraic structures defined are:
-* semirings: rings without opposite for the additive law
-* dioids: idempotent semirings (i.e., forall x, x + x = x)
-* complete dioids: dioids whose canonical order (x <= y wen x + y = y)
-  yields a complete lattice
-* commutative variants (multiplicative law is commutative)
-
-More details can be found in comments at the beginning of each file.
-"""
-
-tags: [
-  "keyword:dioid"
-  "keyword:semiring"
-  "keyword:complete dioid"
-  "category:Miscellaneous/Coq Extensions"
-  "logpath:mathcomp.dioid"
-]
-authors: [
-  "Lucien Rakotomalala <lucien.rakotomalala@onera.fr>"
-  "Pierre Roux <pierre.roux@onera.fr>"
+  "coq-core"
+  "rocq-mathcomp-diod"
 ]
-#url {
-#  src: "https://github.com/validsdp/validsdp/releases/download/v0.8.0/validsdp-0.8.0.tar.gz"
-#  checksum: "sha256=TODO curl -L archive | sha256sum"
-#}
+synopsis: "Compatibility package for rocq-mathcomp-dioid"

rocq-mathcomp-dioid.opam

@@ -0,0 +1,51 @@
+opam-version: "2.0"
+version: "dev"
+maintainer: [
+  "Pierre Roux <pierre.roux@onera.fr>"
+]
+
+homepage: "https://github.com/math-comp/dioid"
+dev-repo: "git+https://github.com/math-comp/dioid.git"
+bug-reports: "https://github.com/math-comp/dioid/issues"
+license: "CECILL-B"
+
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+
+depends: [
+  "rocq-core" { >= "9.0" }
+  "rocq-mathcomp-algebra" { >= "2.6" }
+  "rocq-mathcomp-classical" { >= "1.8" }
+]
+synopsis: "Dioid"
+description: """
+Definitions of the algebraic structure of dioid following the style of
+ssralg in the Mathcomp library.
+
+The main algebraic structures defined are:
+* semirings: rings without opposite for the additive law
+* dioids: idempotent semirings (i.e., forall x, x + x = x)
+* complete dioids: dioids whose canonical order (x <= y wen x + y = y)
+  yields a complete lattice
+* commutative variants (multiplicative law is commutative)
+
+More details can be found in comments at the beginning of each file.
+"""
+
+tags: [
+  "keyword:dioid"
+  "keyword:semiring"
+  "keyword:complete dioid"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:mathcomp.dioid"
+]
+authors: [
+  "Lucien Rakotomalala <lucien.rakotomalala@onera.fr>"
+  "Pierre Roux <pierre.roux@onera.fr>"
+]
+#url {
+#  src: "https://github.com/validsdp/validsdp/releases/download/v0.8.0/validsdp-0.8.0.tar.gz"
+#  checksum: "sha256=TODO curl -L archive | sha256sum"
+#}