New Nix CI setup.

.github/workflows/nix-action.yml

@@ -0,0 +1,41 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Nix CI
+
+on:
+  schedule:
+    - cron: '20 4 * * *'
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        overrides:
+          - 'coq = "master"; mathcomp = "master"'
+          - 'coq = "v8.14"; mathcomp = "master"'
+          - 'coq = "8.13"'
+      fail-fast: false
+    steps:
+      - uses: cachix/install-nix-action@v12
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq
+      - uses: cachix/cachix-action@v8
+        with:
+          name: coq-community
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      - uses: cachix/cachix-action@v8
+        with:
+          name: math-comp
+      - uses: actions/checkout@v2
+      - run: >
+          nix-build https://coq.inria.fr/nix/toolbox --argstr job reglang --arg override '{ ${{ matrix.overrides }}; reglang = builtins.filterSource (path: _: baseNameOf path != ".git") ./.; }'

README.md

@@ -5,6 +5,7 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 # Regular Language Representations in Coq
 
 [![Docker CI][docker-action-shield]][docker-action-link]
+[![Nix CI][nix-action-shield]][nix-action-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
@@ -14,6 +15,9 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [docker-action-shield]: https://github.com/coq-community/reglang/workflows/Docker%20CI/badge.svg?branch=master
 [docker-action-link]: https://github.com/coq-community/reglang/actions?query=workflow:"Docker%20CI"
 
+[nix-action-shield]: https://github.com/coq-community/reglang/workflows/Nix%20CI/badge.svg?branch=master
+[nix-action-link]: https://github.com/coq-community/reglang/actions?query=workflow:"Nix%20CI"
+
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
 

coq-reglang.opam

@@ -19,9 +19,9 @@ 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: [make "-j%{jobs}%" ]
-install: [make "install"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
+  "dune" {>= "2.5"}
   "coq" {(>= "8.10" & < "8.15~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "1.9" & < "1.13~") | (= "dev")}
 ]

meta.yml

@@ -4,6 +4,7 @@ shortname: reglang
 organization: coq-community
 community: true
 action: true
+nix: true
 coqdoc: true
 dune: false
 doi: 10.1007/s10817-018-9460-x
@@ -54,12 +55,17 @@ dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
     version: '{(>= "1.9" & < "1.13~") | (= "dev")}'
-  nix: ssreflect
   description: |-
     [MathComp](https://math-comp.github.io) 1.9.0 or later (`ssreflect` suffices)
 
 tested_coq_nix_versions:
-- version_or_url: https://github.com/coq/coq-on-cachix/tarball/master
+- coq_version: 'master'
+  extra_dev_dependencies:
+  - nix_name: mathcomp
+- coq_version: 'v8.14'
+  extra_dev_dependencies:
+  - nix_name: mathcomp
+- coq_version: '8.13'
 
 tested_coq_opam_versions:
 - version: 'coq-dev'