Switching to the new CoqPackages infrastructure

filtering out packages that are broken

.github/workflows/nix.yml

@@ -8,21 +8,39 @@ jobs:
     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" ]
+        mc: [ "1.12.0", "1.11.0", "1.10.0", "1.9.0", "1.8.0" ]
+        coq: [ "8.13", "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.8.0"
+            coq: "8.13"
+
+          - mc: "1.9.0"
+            coq: "8.11"
           - mc: "1.9.0"
             coq: "8.12"
+          - mc: "1.9.0"
+            coq: "8.13"
+
           - mc: "1.10.0"
             coq: "8.12"
+          - mc: "1.10.0"
+            coq: "8.13"
+
+          - mc: "1.11.0"
+            coq: "8.13"
+
+          - mc: "1.12.0"
+            coq: "8.7"
+          - mc: "1.12.0"
+            coq: "8.8"
+          - mc: "1.12.0"
+            coq: "8.9"
     steps:
       - name: Checkout
         uses: actions/[email protected]
@@ -35,4 +53,5 @@ jobs:
           # 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 }}";}'
+      - run: nix-build --arg override '{coq = "${{ matrix.coq }}"; mathcomp = "${{ matrix.mc }}";}'
+

.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;
+}

.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

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

default.nix

@@ -1,144 +1,19 @@
-{
-  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 = "12dbd4a2f02f2cac2f75337ac6b848e4e037f4de";
+};
 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 = ./.;
+    config = {
+      coq-attribute = if core then "mathcomp-core-shell"
+                      else "mathcomp-full-shell";
+    };
+  } // removeAttrs args ["core"])).nix-auto