Switching to the new CoqPackages infrastructure

- filtering out packages that are broken
- Using ppNixEnv to display the results and put them in README

.github/workflows/nix.yml

@@ -1,38 +1,82 @@
 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@v12
+        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@v12
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
+      - uses: cachix/cachix-action@v8
+        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]
+      - name: Building mathcomp-full-shell target if required
+        run: |
+          overrides="{coq = \"${{ matrix.coq }}\"; mathcomp = \"${{ matrix.mc }}\";}"
+          storepath=$(nix eval "(\"\${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@v12
+        with:
+          nix_path: nixpkgs=channel:nixpkgs-unstable
       - uses: cachix/cachix-action@v8
         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]
+      - name: Update README.md
+        id: set-nixenv
+        run: |
+          ./update-readme.sh
+      - name: Commit README.md
+        uses: EndBug/add-and-commit@v7
+        with:
+          message: 'Updating README.md'
+          add: 'README.md'

README_TEMPLATE.md

@@ -0,0 +1,37 @@
+# Nix support, build and caching for mathcomp packages
+
+![Cachix](https://github.com/math-comp/math-comp-nix/workflows/Cachix/badge.svg)
+
+This caches the builds needed to call
+```
+nix-shell https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz
+
+```
+
+Which can also be called (with some delays in updates)
+```
+nix-shell https://math-comp.github.io/nix
+```
+
+See [Mathcomp on nix Wiki page](https://github.com/math-comp/math-comp/wiki/Using-nix) for a short manual.
+
+## Summary
+
+Here is a synthesis of all available mathcomp packages.
+
+If a mathcomp-coq combination is missing, please add it to the `mc-coq-set` attribute in the file [`matrix/default.nix`](https://github.com/math-comp/math-comp-nix/blob/v2/mstrix/default.nix).
+
+If some mathcomp extra package is missing, there might be two reasons:
+- Either the (upadate of the) package has not been pushed on [NixOS/nixpkgs](https://github.com/NixOS/nixpkgs).
+  If that's the case you can either
+  + open a pull request to add it, or
+  + open an issue and tag @CohenCyril to prompt for the addition of the package.
+- Or the nixpkgs commit has not been updated in https://github.com/coq-nix-toolbox/.
+  In which case, you should go there and run `nix-shell --arg update-nixpkgs true`, commit and push **there**.
+  + This command is also applicable in the current directory but is strongly discouraged
+    outside of development purpose, since it would desynchronize the nixpkgs versions at use
+    between https://github.com/coq-nix-toolbox/ and https://math-comp.github.io/nix.
+  + It can take some time for a package pushed to NixOS/nixpkgs to reach the unstable branch.
+    If you are too impatient you can run `nix-shell --arg do-nothing true --run updateNixpkgsMaster`
+    **on your own projects**.
+

ci-matrix.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+cat $(nix-build --no-build-output matrix)

default.nix

@@ -1,144 +1,20 @@
-{
-  nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix
-             else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/502845c3e31ef3de0e424f3fcb09217df2ce6df6.tar.gz),
-  config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}),
-  withEmacs ? false,
-  print-env ? false,
-  do-nothing ? false,
-  package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"),
-  src ? (if builtins.pathExists ./package.nix then ./. else false)
-}:
-with builtins;
-let
-  cfg-fun = if isFunction config then config else (pkgs: config);
-  pkg-src = if src == false then {}
-            else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; };
-  pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs {
-    overlays = [ (pkgs: super-pkgs: with pkgs.lib;
-      let coqPackages = with pkgs; {
-        "8.7" = coqPackages_8_7;
-        "8.8" = coqPackages_8_8;
-        "8.9" = coqPackages_8_9;
-        "8.10" = coqPackages_8_10;
-        "8.11" = coqPackages_8_11;
-        "8.12" = coqPackages_8_12;
-        "default" = coqPackages_8_10;
-      }.${(cfg-fun pkgs).coq or "default"}.overrideScope'
-        (coqPackages: super-coqPackages:
-          let
-            all-pkgs = pkgs // { inherit coqPackages; };
-            cfg = pkg-src // {
-              mathcomp-fast = {
-                src = ./.;
-                propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast);
-              };
-              mathcomp-full = {
-                src = ./.;
-                propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all);
-              };
-            } // (cfg-fun all-pkgs);
-          in {
-            mathcomp-extra-config =
-              let mec = super-coqPackages.mathcomp-extra-config; in
-              lib.recursiveUpdate mec {
-                initial = {
-                  # fixing mathcomp analysis to depend on real-closed
-                  mathcomp-analysis = {version, coqPackages} @ args:
-                    let mca = mec.initial.mathcomp-analysis args; in
-                    mca // {
-                      propagatedBuildInputs = mca.propagatedBuildInputs ++
-                                              (if builtins.elem coq.version ["8.10" "8.11" "8.12"] then (with coqPackages; [ coq-elpi hierarchy-builder ]) else []);
-                    };
-                };
-                for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} =
-                  (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) //
-                  (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]);
-              };
-            mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp;
-          } // mapAttrs
-            (package: version: coqPackages.mathcomp-extra package version)
-            (removeAttrs cfg ["mathcomp" "coq"])
-        ); in {
-          coqPackages = coqPackages.filterPackages coqPackages.coq coqPackages;
-          coq = coqPackages.coq;
-          mc-clean = src: {
-            version = baseNameOf src;
-            src = cleanSourceWith {
-              src = cleanSource src;
-              filter = path: type: let baseName = baseNameOf (toString path); in ! (
-                hasSuffix ".aux" baseName ||
-                hasSuffix ".d" baseName ||
-                hasSuffix ".vo" baseName ||
-                hasSuffix ".glob" baseName ||
-                elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"]
-              );
-            };
-          };
-        })];
-  };
-
-  mathcompnix = ./.;
-
-  shellHook = ''
-    nixEnv () {
-      echo "Here is your work environement"
-      echo "buildInputs:"
-      for x in $buildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
-      echo "propagatedBuildInputs:"
-      for x in $propagatedBuildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
-      echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions"
-    }
-
-    printEnv () {
-      for x in $buildInputs; do echo $x; done
-      for x in $propagatedBuildInputs; do echo $x; done
-    }
-
-    cachixEnv () {
-      echo "Pushing environement to cachix"
-      printEnv | cachix push math-comp
-    }
-
-    nixDefault () {
-      cat $mathcompnix/default.nix
-    } > default.nix
-
-    updateNixPkgs (){
-      HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1);
-      URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz
-      SHA256=$(nix-prefetch-url --unpack $URL)
-      echo "fetchTarball {
-        url = $URL;
-        sha256 = \"$SHA256\";
-      }" > nixpkgs.nix
-    }
-    updateNixPkgsMaster (){
-      HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1);
-      URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz
-      SHA256=$(nix-prefetch-url --unpack $URL)
-      echo "fetchTarball {
-        url = $URL;
-        sha256 = \"$SHA256\";
-      }" > nixpkgs.nix
-    }
-  ''
-  + pkgs.lib.optionalString print-env "nixEnv";
-
-  emacs = with pkgs; emacsWithPackages
-    (epkgs: with epkgs.melpaStablePackages; [proof-general]);
-
-  pkg = with pkgs;
-        if package == "mathcomp.single" then coqPackages.mathcomp.single
-        else coqPackages.${package} or (coqPackages.current-mathcomp-extra package);
+{ core ? false,
+  config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false, ci-step ? null,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  ci ? (!isNull ci-step), inNixShell ? null
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/nix-toolbox.git";
+  ref = "master";
+  rev = "b1e5c52bdc1d79b7cd220476ebd9bc552a2331c7";
+};
 in
-if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: {
-  inherit shellHook mathcompnix;
-
-  buildInputs = if do-nothing then []
-                else (old.buildInputs ++
-                (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs
-                 else []));
-
-  propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs;
-
-}) else pkg
+(import auto (
+  { src = ./shells;
+    config = {
+      coq-attribute = if core then "mathcomp-core-shell"
+                      else "mathcomp-full-shell";
+
+    };
+  } // removeAttrs args ["core"])).nix-auto

matrix/default.nix

@@ -0,0 +1,36 @@
+{ run ? null }:
+with import <nixpkgs> {}; with builtins; with lib;
+let
+  old-coq = [ "8.9" "8.8" "8.7" ];
+  mc-coq-set = {
+    "1.12.0" = [ "8.13" "8.12" "8.11" "8.10" ];
+    "1.11.0" = [ "8.12" "8.11" "8.10" ] ++ old-coq;
+    "1.10.0" = [ "8.11" "8.10" ] ++ old-coq;
+    "1.9.0" =  [ "8.10" ] ++ old-coq;
+    "1.8.0" =  old-coq;
+  };
+
+  mcs   = sort versionAtLeast (attrNames mc-coq-set);
+  pairs = mc: map (coq: { inherit mc coq; })
+                  (sort versionAtLeast mc-coq-set.${mc});
+  matrix.include = flatten (map pairs mcs);
+
+  # Generating an expanded script
+  coq-loop = coq: ''
+    export coq="${coq}"
+  '' + run + "\n";
+  mc-loop = mc: ''
+    export mc="${mc}"
+  '' + foldl (sh: coq: sh + coq-loop coq) "" mc-coq-set.${mc};
+in
+
+if !isString run then
+  writeTextFile {
+    name = "JSONMatrix";
+    text = toJSON matrix;
+  }
+else
+writeScriptBin "run" (''
+    #!/usr/bin/env bash
+    '' + foldl (sh: mc: sh + mc-loop mc) "" mcs)
+

matrix/report.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+echo "### Mathematical Components $mc and Coq $coq"
+nix-shell ./. --arg override "{coq = \"$coq\"; mathcomp = \"$mc\";}" --run ppNixEnv

shells/.nix/coq-overlays/mathcomp-core-shell/default.nix

@@ -0,0 +1,6 @@
+{ stdenv, coq, mathcomp, version ? null }@args:
+stdenv.mkDerivation {
+  name = "mathcomp-core-shell";
+  buildInputs = [ coq mathcomp ];
+  src = version;
+}

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

@@ -0,0 +1,9 @@
+{ 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 = version;
+}

Makefile → shells/Makefile

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

update-readme.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+cat README_TEMPLATE.md > README.md
+$(nix-build matrix --no-build-output --argstr run "bash matrix/report.sh")/bin/run >> README.md