Revert "Use nix-tool-box"

This reverts commit 8674d6996fca76028ead3f75363f11bab4fa3e7c that I
added by accident

8 files changed, 179 insertions, 123 deletions

diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
deleted file mode 100644
index f31495f..0000000
--- a/.github/workflows/nix-action.yml
+++ /dev/null
@@ -1,74 +0,0 @@
-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)}}
-    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 "${{ matrix.task }}" --argstr ci-job dependencies
-    - name: Building/fetching current project
-      run: nix-build --argstr ci "${{ matrix.task }}" --argstr ci-job main
-
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
new file mode 100644
index 0000000..6a34426
--- /dev/null
+++ b/.github/workflows/nix.yml
@@ -0,0 +1,32 @@
+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
deleted file mode 100644
index dde76b9..0000000
--- a/.nix/config.nix
+++ /dev/null
@@ -1,34 +0,0 @@
-{
-  ## 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
-  coq-shell-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";
-  tasks."coq-8.10".coqPackages.coq.override.version = "8.10";
-}
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
deleted file mode 100644
index ba2d943..0000000
--- a/.nix/coq-nix-toolbox.nix
+++ /dev/null
@@ -1 +0,0 @@
-"e54b920493f0494ede95b5f7d083cc8b20b1f5a6"
diff --git a/.nix/coq-overlays/mathcomp-single/default.nix b/.nix/coq-overlays/mathcomp-single/default.nix
deleted file mode 100644
index 65be1c4..0000000
--- a/.nix/coq-overlays/mathcomp-single/default.nix
+++ /dev/null
@@ -1,2 +0,0 @@
-{ mathcomp, version ? null }:
-mathcomp.override {single = true; version = null;}
diff --git a/config.nix b/config.nix
new file mode 100644
index 0000000..bb1ecee
--- /dev/null
+++ b/config.nix
@@ -0,0 +1,3 @@
+{
+  coq = "8.11";
+}
diff --git a/default.nix b/default.nix
index a588f43..195a47e 100644
--- a/default.nix
+++ b/default.nix
@@ -1,13 +1,144 @@
-{ 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;
-};
+{
+  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);
 in
-(import auto ({inherit src;} // args)).nix-auto
+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
diff --git a/package.nix b/package.nix
new file mode 100644
index 0000000..661824d
--- /dev/null
+++ b/package.nix
@@ -0,0 +1 @@
+"mathcomp.single"