remove Dune requirement for now, add CI for MathComp 1.12 (#23)

.github/workflows/coq-action.yml

@@ -16,6 +16,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
           - 'mathcomp/mathcomp:1.11.0-coq-8.12'
           - 'mathcomp/mathcomp:1.10.0-coq-8.11'
           - 'mathcomp/mathcomp:1.9.0-coq-8.10'

README.md

@@ -44,7 +44,6 @@ decidability results and closure properties of regular languages.
 - Compatible Coq versions: 8.10 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.9.0 or later (`ssreflect` suffices)
-  - [Dune](https://dune.build) 2.5 or later
 - Coq namespace: `RegLang`
 - Related publication(s):
   - [Regular Language Representations in the Constructive Type Theory of Coq](https://hal.archives-ouvertes.fr/hal-01832031/document) doi:[10.1007/s10817-018-9460-x](https://doi.org/10.1007/s10817-018-9460-x)
@@ -64,8 +63,8 @@ To instead build and install manually, do:
 ``` shell
 git clone https://github.com/coq-community/reglang.git
 cd reglang
-dune build
-dune install
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
 ```
 
 

coq-reglang.opam

@@ -16,11 +16,11 @@ automata (deterministic, nondeterministic, one-way, two-way),
 regular expressions, and the logic WS1S. It also contains various
 decidability results and closure properties of regular languages."""
 
-build: ["dune" "build" "-p" name "-j" jobs]
+build: [make "-j%{jobs}%" ]
+install: [make "install"]
 depends: [
-  "dune" {>= "2.5"}
   "coq" {(>= "8.10" & < "8.13~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.9" & < "1.12~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.9" & < "1.13~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -5,6 +5,7 @@ organization: coq-community
 community: true
 action: true
 coqdoc: true
+dune: false
 doi: 10.1007/s10817-018-9460-x
 
 synopsis: >-
@@ -41,8 +42,6 @@ opam-file-maintainer: palmskog@gmail.com
 
 opam-file-version: dev
 
-dune: true
-
 license:
   fullname: CeCILL-B
   identifier: CECILL-B
@@ -54,7 +53,7 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.9" & < "1.12~") | (= "dev")}'
+    version: '{(>= "1.9" & < "1.13~") | (= "dev")}'
   nix: ssreflect
   description: |-
     [MathComp](https://math-comp.github.io) 1.9.0 or later (`ssreflect` suffices)
@@ -65,6 +64,8 @@ tested_coq_nix_versions:
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '1.12.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
 - version: '1.11.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
 - version: '1.10.0-coq-8.11'