Use nix-tool-box

8 files changed, 155 insertions, 179 deletions

diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
new file mode 100644
index 0000000..dc920d9
--- /dev/null
+++ b/.github/workflows/nix-action.yml
@@ -0,0 +1,107 @@
+name: Nix CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  dependencies:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching dependencies
+      run: nix-build --argstr ci-job dependencies
+    - name: Setup build matrix
+      id: set-matrix
+      run: |
+        matrix=$(nix-shell --arg do-nothing true --run nixTasks)
+        echo ::set-output name=matrix::{\"task\":$(echo $matrix)}\"
+
+  main:
+    runs-on: ubuntu-latest
+    needs:
+    - dependencies
+    strategy:
+      matrix: ${{fromJson(needs.dependencies.outputs.matrix)}}
+      fail-fast: false
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching dependencies
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies
+    - name: Building/fetching current project
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job main
+
+  shell:
+    runs-on: ubuntu-latest
+    needs:
+    - dependencies
+    strategy:
+      matrix: ${{fromJson(needs.dependencies.outputs.matrix)}}
+      fail-fast: false
+    steps:
+    - name: Cachix install
+      uses: cachix/install-nix-action@v12
+      with:
+        nix_path: nixpkgs=channel:nixpkgs-unstable
+    - name: Cachix setup coq
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: coq
+    - name: Cachix setup math-comp
+      uses: cachix/cachix-action@v8
+      with:
+        # Name of a cachix cache to pull/substitute
+        name: math-comp
+        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+    - name: Git checkout
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+    - name: Building/fetching dependencies
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job dependencies
+    - name: Building/fetching current project
+      run: nix-build --no-out-link --argstr ci "${{ matrix.task }}" --argstr ci-job shell
+
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
deleted file mode 100644
index 6a34426..0000000
--- a/.github/workflows/nix.yml
+++ /dev/null
@@ -1,32 +0,0 @@
-name: Cachix
-on:
-  push:
-jobs:
-  cachix:
-    name: Cachix branch
-    runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        coq: [ "8.11", "8.12" ]
-    steps:
-      - name: Get branch shortname
-        run: echo "##[set-output name=name;]$(echo ${GITHUB_REF#refs/heads/})"
-        id: branch-short
-      - name: Get owner name
-        run: echo "##[set-output name=name;]$(echo $GITHUB_REPOSITORY | cut -d/ -f1)"
-        id: owner
-      - name: Get owner lowercase name
-        run: echo "##[set-output name=name;]$(echo $GITHUB_REPOSITORY | cut -d/ -f1 | tr '[:upper:]' '[:lower:]')"
-        id: owner-lowercase
-      - uses: cachix/install-nix-action@v12
-      - uses: cachix/cachix-action@v8
-        if: steps.owner.outputs.name == 'math-comp' || steps.owner.outputs.name == 'CohenCyril'
-        with:
-          # Name of a cachix cache to push and pull/substitute
-          name: ${{ steps.owner-lowercase.outputs.name }}
-          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 https://github.com/math-comp/math-comp-nix/archive/master.tar.gz --arg config '{coq = "${{ matrix.coq }}"; mathcomp = "${{ steps.owner.outputs.name }}/${{ steps.branch-short.outputs.name }}";}' --argstr package mathcomp
diff --git a/.nix/config.nix b/.nix/config.nix
new file mode 100644
index 0000000..5656f01
--- /dev/null
+++ b/.nix/config.nix
@@ -0,0 +1,33 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build, either from nixpkgs
+  ## of from the overlays located in `.nix/coq-overlays`
+  coq-attribute = "mathcomp";
+
+  ## If you want to select a different attribute
+  ## to serve as a basis for nix-shell edit this
+  shell-coq-attribute = "mathcomp-single";
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  coqproject = "mathcomp/_CoqProject";
+
+  ## select an entry to build in the following `tasks` set
+  ## defaults to "default"
+  select = "coq-8.13";
+
+  ## write one `tasks.name` attribute set per
+  ## alternative configuration, the can be used to
+  ## compute several ci jobs as well
+
+  ## You can override Coq and other Coq coqPackages
+  ## through the following attribute
+
+  tasks."coq-8.13".coqPackages.coq.override.version = "8.13";
+  tasks."coq-8.12".coqPackages.coq.override.version = "8.12";
+  tasks."coq-8.11".coqPackages.coq.override.version = "8.11";
+}
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
new file mode 100644
index 0000000..4267323
--- /dev/null
+++ b/.nix/coq-nix-toolbox.nix
@@ -0,0 +1 @@
+"6bc8d19328c17c44d787da39b1794255cd244008"
diff --git a/.nix/coq-overlays/mathcomp-single/default.nix b/.nix/coq-overlays/mathcomp-single/default.nix
new file mode 100644
index 0000000..65be1c4
--- /dev/null
+++ b/.nix/coq-overlays/mathcomp-single/default.nix
@@ -0,0 +1,2 @@
+{ mathcomp, version ? null }:
+mathcomp.override {single = true; version = null;}
diff --git a/config.nix b/config.nix
deleted file mode 100644
index bb1ecee..0000000
--- a/config.nix
+++ /dev/null
@@ -1,3 +0,0 @@
-{
-  coq = "8.11";
-}
diff --git a/default.nix b/default.nix
index 195a47e..a588f43 100644
--- a/default.nix
+++ b/default.nix
@@ -1,144 +1,13 @@
-{
-  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);
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false, ci-job ? null,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  ci ? (!isNull ci-job), inNixShell ? null, src ? ./.,
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/coq-nix-toolbox.git";
+  ref = "master";
+# putting a ref here is strongly advised
+  rev = import .nix/coq-nix-toolbox.nix;
+};
 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 [])) ++ [ pkgs.lua pkgs.sedutil ];
-
-  propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs;
-
-}) else pkg
+(import auto ({inherit src;} // args)).nix-auto
diff --git a/package.nix b/package.nix
deleted file mode 100644
index 661824d..0000000
--- a/package.nix
+++ /dev/null
@@ -1 +0,0 @@
-"mathcomp.single"