Merge pull request #21 from coq-community/action

switch to GitHub actions / regenerate from templates

.github/workflows/coq-action.yml

@@ -0,0 +1,32 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.10.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.9.0-coq-8.10'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-reglang.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -1,14 +1,14 @@
 # Regular Language Representations in Coq
 
-[![Travis][travis-shield]][travis-link]
+[![CI][action-shield]][action-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 [![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
-[travis-shield]: https://travis-ci.com/coq-community/reglang.svg?branch=master
-[travis-link]: https://travis-ci.com/coq-community/reglang/builds
+[action-shield]: https://github.com/coq-community/reglang/workflows/CI/badge.svg?branch=master
+[action-link]: https://github.com/coq-community/reglang/actions?query=workflow%3ACI
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -44,6 +44,7 @@ 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)
@@ -63,8 +64,8 @@ To instead build and install manually, do:
 ``` shell
 git clone https://github.com/coq-community/reglang.git
 cd reglang
-make   # or make -j <number-of-cores-on-your-machine>
-make install
+dune build
+dune install
 ```
 
 

default.nix

@@ -11,15 +11,6 @@ in
 
 with coqPackages;
 
-let
-  ssreflect =
-    coqPackages.ssreflect.overrideAttrs(_: rec {
-      name = "coq-${coq.coq-version}-ssreflect-${version}";
-      version = "dev";
-      src = fetchTarball "https://github.com/math-comp/math-comp/tarball/master";
-    });
-in
-
 pkgs.stdenv.mkDerivation {
 
   name = "reglang";

meta.yml

@@ -3,7 +3,7 @@ fullname: Regular Language Representations in Coq
 shortname: reglang
 organization: coq-community
 community: true
-travis: true
+action: true
 coqdoc: true
 doi: 10.1007/s10817-018-9460-x
 
@@ -41,6 +41,8 @@ opam-file-maintainer: palmskog@gmail.com
 
 opam-file-version: dev
 
+dune: true
+
 license:
   fullname: CeCILL-B
   identifier: CECILL-B

theories/misc.v

@@ -139,7 +139,12 @@ Proof.
 Qed.
 
 Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT.
-Proof. move/(inj_card_bij val_inj) => [g g1 g2 x]. rewrite -(g2 x). exact: valP. Qed.
+Proof.
+  (* backwards compatible fix for mathcomp PR #626 - mathcomp-1.12.0 *)
+  move=> eq_pT; have [|g g1 g2 x] := @inj_card_bij [finType of (sig p)] T _ val_inj.
+    by rewrite eq_pT.
+  rewrite -(g2 x); exact: valP.
+Qed.
 
 (** Finite Ordinals *)
 
@@ -244,8 +249,8 @@ Qed.
 Lemma surj_card_bij (T T' : finType) (f : T -> T') :
   surjective f -> #|T| = #|T'| -> bijective f.
 Proof.
-  move => S E. apply: inj_card_bij (E). apply/injectiveP. change (uniq (codom f)).
-  apply/card_uniqP. rewrite size_map -cardT E. exact: surjectiveE.
+  move => S E. apply: inj_card_bij; last by rewrite E. 
+  apply/injectiveP; apply/card_uniqP. rewrite size_map -cardT E. exact: surjectiveE.
 Qed.
 
 (* We define a general inverse of surjective functions from choiceType -> eqType.
@@ -256,7 +261,5 @@ Definition cr {X : choiceType} {Y : eqType} {f : X -> Y} (Sf : surjective f) y :
 Lemma crK {X : choiceType} {Y : eqType} {f : X->Y} {Sf : surjective f} x: f (cr Sf x) = x.
 Proof. by rewrite (eqP (xchooseP (Sf x))). Qed.
 
-
-
 Lemma dec_eq (P : Prop) (decP : decidable P) : decP <-> P.
 Proof. by case: decP. Qed.