Merge pull request #128 from hoheinzollern/rocq_build

Rocq build

Author: proux01

.github/workflows/docker-action.yml

@@ -26,7 +26,7 @@ jobs:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-mathcomp-finmap.opam'
+          opam_file: 'rocq-mathcomp-finmap.opam'
           custom_image: ${{ matrix.image }}
 
 

Makefile.common

@@ -6,9 +6,10 @@
 # pre-makefile::, this-clean:: and __always__:: may be extended      #
 # Additionally, the following variables may be customized:           #
 SUBDIRS?=
-COQBIN?=$(dir $(shell which coqtop))
-COQMAKEFILE?=$(COQBIN)coq_makefile
-COQDEP?=$(COQBIN)coqdep
+
+COQBIN?=$(dir $(shell command -v coqtop || command -v rocq))
+COQMAKEFILE?=$(shell command -v coq_makefile || echo "$(COQBIN)rocq makefile")
+COQDEP?=$(shell command -v coqdep || echo "$(COQBIN)rocq dep")
 COQPROJECT?=_CoqProject
 COQMAKEOPTIONS?=
 COQMAKEFILEOPTIONS?=

coq-mathcomp-finmap.opam

@@ -1,31 +1,13 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
-maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
 version: "dev"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
 
-homepage: "https://github.com/math-comp/finmap"
-dev-repo: "git+https://github.com/math-comp/finmap.git"
+homepage: "https://math-comp.github.io/"
 bug-reports: "https://github.com/math-comp/finmap/issues"
+dev-repo: "git+https://github.com/math-comp/finmap.git"
 license: "CECILL-B"
 
-synopsis: "Finite sets, finite maps, finitely supported functions"
-description: """
-This library is an extension of mathematical component in order to
-support finite sets and finite maps on choicetypes (rather that finite
-types). This includes support for functions with finite support and
-multisets. The library also contains a generic order and set libary,
-which will be used to subsume notations for finite sets, eventually."""
-
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-depends: [
-  ("coq" {>= "8.20" & < "8.21~"}
-  | "rocq-core" {>= "9.0" | = "dev"})
-  "coq-mathcomp-ssreflect" { (>= "2.0" & < "2.5~") | = "dev" }
-]
-
+depends: [ "rocq-mathcomp-finmap" { = version } ]
 tags: [
   "keyword:finmap"
   "keyword:finset"
@@ -36,3 +18,5 @@ authors: [
   "Cyril Cohen"
   "Kazuhiko Sakaguchi"
 ]
+
+synopsis: "Compatibility package for rocq-mathcomp-finmap"

meta.yml

@@ -1,7 +1,7 @@
 fullname: Finite maps
 shortname: finmap
 organization: math-comp
-opam_name: coq-mathcomp-finmap
+opam_name: rocq-mathcomp-finmap
 community: false
 action: true
 coqdoc: false
@@ -46,8 +46,8 @@ tested_coq_opam_versions:
 
 dependencies:
 - opam:
-    name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.0" & < "2.4~") | (= "dev") }'
+    name: rocq-mathcomp-ssreflect
+    version: '{ (>= "2.0" & < "2.5~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.0 to 2.3](https://math-comp.github.io)
 

rocq-mathcomp-finmap.opam

@@ -0,0 +1,39 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+version: "dev"
+
+homepage: "https://github.com/math-comp/finmap"
+dev-repo: "git+https://github.com/math-comp/finmap.git"
+bug-reports: "https://github.com/math-comp/finmap/issues"
+license: "CECILL-B"
+
+synopsis: "Finite sets, finite maps, finitely supported functions"
+description: """
+This library is an extension of mathematical component in order to
+support finite sets and finite maps on choicetypes (rather that finite
+types). This includes support for functions with finite support and
+multisets. The library also contains a generic order and set libary,
+which will be used to subsume notations for finite sets, eventually."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  ("coq" {>= "8.20" & < "8.21~"}
+  | "rocq-core" {>= "9.0" | = "dev"})
+  ("coq-mathcomp-ssreflect" { >= "2.0" & < "2.4~" }
+  |"rocq-mathcomp-ssreflect" { (>= "2.4" & < "2.5~") | = "dev" })
+]
+
+tags: [
+  "keyword:finmap"
+  "keyword:finset"
+  "keyword:multiset"
+  "logpath:mathcomp.finmap"
+]
+authors: [
+  "Cyril Cohen"
+  "Kazuhiko Sakaguchi"
+]