V2

.github/workflows/nix.yml

@@ -1,38 +1,85 @@
 name: Cachix
 on:
-  push:
+  pull_request:
+    branches:
+      - master
+      - v2
 jobs:
-  cachix:
-    name: Cachix branch
+  setup:
+    name: Computing matrix of tested versions
     runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - name: Checkout
+        uses: actions/[email protected]
+      - uses: cachix/install-nix-action@v21
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - name: Setup build matrix
+        id: set-matrix
+        run: "echo ::set-output name=matrix::$(./ci-matrix.sh)"
+
+  builds:
+    name: Build mathcomp and coq combination
+    runs-on: ubuntu-latest
+    needs: setup
     strategy:
       fail-fast: false
-      matrix:
-        mc: [ "1.11.0", "1.10.0", "1.9.0", "1.8.0" ]
-        coq: [ "8.12", "8.11", "8.10", "8.9", "8.8", "8.7" ]
-        exclude:
-          - mc: "1.8.0"
-            coq: "8.10"
-          - mc: "1.8.0"
-            coq: "8.11"
-          - mc: "1.9.0"
-            coq: "8.11"
-          - mc: "1.8.0"
-            coq: "8.12"
-          - mc: "1.9.0"
-            coq: "8.12"
-          - mc: "1.10.0"
-            coq: "8.12"
+      matrix: ${{fromJson(needs.setup.outputs.matrix)}}
     steps:
+      - uses: cachix/install-nix-action@v21
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v12
+        with:
+          # Name of a cachix cache to push and pull/substitute
+          name:  math-comp
+          extraPullNames: coq
+          # Authentication token for Cachix, needed only for private cache access
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
       - name: Checkout
-        uses: actions/[email protected]
-      - uses: cachix/install-nix-action@v12
-      - uses: cachix/cachix-action@v8
+        uses: actions/[email protected]
+      - name: Building mathcomp-full-shell target if required
+        run: |
+          overrides="{coq = \"${{ matrix.coq }}\"; mathcomp = \"${{ matrix.mc }}\";}"
+          storepath=$(nix eval --impure --expr "(\"\${import ./. {override = $overrides;}}\")")
+          hash=$(echo $storepath | sed "s/\"//mg" | xargs basename | cut -d- -f1)
+          url=https://math-comp.cachix.org/$hash.narinfo
+          if curl --output /dev/null --silent --head --fail "$url"; then
+            echo "In cache: $url, doing nothing"
+          else
+            echo "Not in cache, compiling"
+            nix-build --no-out-link --arg override "$overrides"
+          fi
+
+  summary:
+    name: Generate summary
+    runs-on: ubuntu-latest
+    needs: builds
+    steps:
+      - uses: cachix/install-nix-action@v21
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v12
         with:
           # Name of a cachix cache to push and pull/substitute
           name:  math-comp
           extraPullNames: coq
           # Authentication token for Cachix, needed only for private cache access
           authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-      # building fake mathcomp-fast target
-      - run: nix-build --arg config '{coq = "${{ matrix.coq }}"; mathcomp = "${{ matrix.mc }}";}'
+      ## does not work because the PR is updated only once
+      - name: Checkout
+        uses: actions/[email protected]
+        with:
+          repository: ${{ github.event.pull_request.head.repo.full_name }}
+          ref: ${{ github.event.pull_request.head.ref }}
+      - name: Update README.md
+        id: set-nixenv
+        run: |
+          ./update-readme.sh
+      - name: Commit README.md
+        uses: EndBug/add-and-commit@v9
+        with:
+          message: 'Updating README.md'
+          add: 'README.md'

.nix/config.nix

@@ -0,0 +1,103 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build from the local sources,
+  ## either using nixpkgs data or the overlays located in `.nix/coq-overlays`
+  ## Will determine the default main-job of the bundles defined below
+  attribute = "mathcomp-full-shell";
+
+  ## If you want to select a different attribute (to build from the local sources as well)
+  ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
+  # shell-attribute = "{{nix_name}}";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  # pname = "{{shortname}}";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
+  # buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  # coqproject = "_CoqProject";
+
+  ## select an entry to build in the following `bundles` set
+  ## defaults to "default"
+  default-bundle = "default";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+  bundles.default = {
+
+    ## You can override Coq and other Coq coqPackages
+    ## through the following attribute
+    # coqPackages.coq.override.version = "8.11";
+
+    ## In some cases, light overrides are not available/enough
+    ## in which case you can use either
+    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
+    ## or a "long" overlay to put in `.nix/coq-overlays
+    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
+    ## to automatically retrieve the one from nixpkgs
+    ## if it exists and is correctly named/located
+
+    ## You can override Coq and other coqPackages
+    ## through the following attribute
+    ## If <ocaml-pkg> does not support light overrides,
+    ## you may use `overrideAttrs` or long overlays
+    ## located in `.nix/ocaml-overlays`
+    ## (there is no automation for this one)
+    #  ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
+
+    ## You can also override packages from the nixpkgs toplevel
+    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
+    ## Or put an overlay in `.nix/overlays`
+
+    ## you may mark a package as a main CI job (one to take deps and
+    ## rev deps from) as follows
+    # coqPackages.<main-pkg>.main-job = true;
+    ## by default the current package and its shell attributes are main jobs
+
+    ## you may mark a package as a CI job as follows
+    #  coqPackages.<another-pkg>.job = "test";
+    ## It can then built through
+    ## nix-build --argstr bundle "default" --arg job "test";
+    ## in the absence of such a directive, the job "another-pkg" will
+    ## is still available, but will be automatically included in the CI
+    ## via the command genNixActions only if it is a dependency or a
+    ## reverse dependency of a job flagged as "main-job" (see above).
+
+    ## Run on push on following branches (default [ "master" ])
+    # push-branches = [ "master" "branch2" ];
+  };
+
+  ## Cachix caches to use in CI
+  ## Below we list some standard ones
+  cachix.coq = {};
+  cachix.math-comp = {};
+  cachix.coq-community = {};
+
+  ## If you have write access to one of these caches you can
+  ## provide the auth token or signing key through a secret
+  ## variable on GitHub. Then, you should give the variable
+  ## name here. For instance, coq-community projects can use
+  ## the following line instead of the one above:
+  # cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
+
+  ## Or if you have a signing key for a given Cachix cache:
+  # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
+
+  ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
+  ## are the names of secret variables. They are set in
+  ## GitHub's web interface.
+}

.nix/coq-nix-toolbox.nix

@@ -0,0 +1 @@
+"f0370efea6403ad3862e379fdd0892ed5a295d55"

Makefile → .nix/coq-overlays/mathcomp-full-shell/Makefile

@@ -1,3 +1,5 @@
 .PHONY: err
 err:
 	echo "Use --arg src /your/path to provide a source path"
+install:
+	echo "No install"

.nix/coq-overlays/mathcomp-full-shell/default.nix

@@ -0,0 +1,11 @@
+{ stdenv,
+  coq, mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  mathcomp-real-closed, mathcomp-analysis, multinomials,
+  mathcomp-abel, version ? null }@args:
+stdenv.mkDerivation {
+  name = "mathcomp-full-shell";
+  buildInputs =
+    with builtins; filter (x: !(x.meta.broken or false))
+      (attrValues (removeAttrs args ["stdenv" "version"]));
+  src = ./.;
+}

.nix/nixpkgs.nix

@@ -0,0 +1,4 @@
+fetchTarball {
+         url = https://github.com/CohenCyril/nixpkgs/archive/8c2fccc525426a1ac5370b8748756934e20e20bf.tar.gz;
+         sha256 = "18zr88g3p7x4dhldxqzzxn56fq5qvh5vwcy5g7kgq7n3kvaqpk3r";
+       }