update opam and ci for MathComp 1.13.0, adjust dune boilerplate (coq-…

…community#35)

.github/workflows/docker-action.yml

@@ -20,6 +20,8 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'
           - 'mathcomp/mathcomp:1.12.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'

.github/workflows/nix-action.yml

@@ -20,35 +20,30 @@ jobs:
       matrix:
         overrides:
           - 'coq = "master"; mathcomp = "master"'
-          - 'coq = "v8.14"; mathcomp = "master"'
+          - 'coq = "8.14"'
           - 'coq = "8.13"'
       fail-fast: false
     steps:
-      - name: Determine which ref to test
+      - name: Determine which commit to test
         run: |
           if [[ ${{ github.event_name }} =~ "pull_request" ]]; then
             merge_commit=$(git ls-remote ${{ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge | cut -f1)
             if [ -z "$merge_commit" ]; then
-              echo "tested_ref=refs/pull/${{ github.event.number }}/head" >> $GITHUB_ENV
+              echo "tested_commit=${{ github.event.pull_request.head.sha }}" >> $GITHUB_ENV
             else
-              echo "tested_ref=refs/pull/${{ github.event.number }}/merge" >> $GITHUB_ENV
+              echo "tested_commit=$merge_commit" >> $GITHUB_ENV
             fi
           else
-            echo "tested_ref=${{ github.ref }}" >> $GITHUB_ENV
+            echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV
           fi
-      - uses: cachix/install-nix-action@v12
+      - uses: cachix/install-nix-action@v14
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
-      - uses: cachix/cachix-action@v8
-        with:
-          name: coq
-      - uses: cachix/cachix-action@v8
+      - uses: cachix/cachix-action@v10
         with:
           name: coq-community
           authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-      - uses: cachix/cachix-action@v8
-        with:
-          name: math-comp
+          extraPullNames: coq, math-comp
       - uses: actions/checkout@v2
         with:
           ref: ${{ env.tested_ref }}

.gitignore

@@ -14,3 +14,4 @@ Makefile.coq.conf
 .coq-native/
 _build/
 docs/
+.lia.cache

coq-reglang.opam

@@ -1,6 +1,3 @@
-# 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: "[email protected]"
 version: "dev"
@@ -23,7 +20,7 @@ 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")}
+  "coq-mathcomp-ssreflect" {(>= "1.9" & < "1.14~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -54,22 +54,24 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.9" & < "1.13~") | (= "dev")}'
+    version: '{(>= "1.9" & < "1.14~") | (= "dev")}'
   description: |-
     [MathComp](https://math-comp.github.io) 1.9.0 or later (`ssreflect` suffices)
 
 tested_coq_nix_versions:
 - coq_version: 'master'
   extra_dev_dependencies:
   - nix_name: mathcomp
-- coq_version: 'v8.14'
-  extra_dev_dependencies:
-  - nix_name: mathcomp
+- coq_version: '8.14'
 - coq_version: '8.13'
 
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '1.13.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.13'

theories/dune

@@ -2,4 +2,4 @@
  (name RegLang)
  (package coq-reglang)
  (synopsis "Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp")
- (flags -w -notation-overridden -w -duplicate-clear -w -notation-incompatible-format -w -deprecated-instance-without-locality))
+ (flags :standard -w -notation-overridden -w -duplicate-clear -w -notation-incompatible-format -w -deprecated-instance-without-locality))