add a hierarchy of structures to measure.v

math-comp · Nov 17, 2020 · 61a92cc · 61a92cc
1 parent e3b82be
commit 61a92cc
Show file tree

Hide file tree

Showing 4 changed files with 631 additions and 126 deletions.
diff --git a/config.nix b/config.nix
@@ -1,5 +1,6 @@
 {
-  coq = "8.10";
+  coq = "8.11";
   mathcomp = "mathcomp-1.11.0";
   mathcomp-real-closed = "1.1.1";
+  hierarchy-builder = "0.10.0";
 }
diff --git a/default.nix b/default.nix
@@ -1,9 +1,10 @@
 {
   nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix
-             else fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-fix-rec.tar.gz),
+             else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/72b9660dc18ba347f7cd41a9504fc181a6d87dc3.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)
 }:
@@ -20,7 +21,8 @@ let
         "8.9" = coqPackages_8_9;
         "8.10" = coqPackages_8_10;
         "8.11" = coqPackages_8_11;
-        "default" = coqPackages_8_10;
+        "8.12" = coqPackages_8_12;
+        "default" = coqPackages_8_11;
       }.${(cfg-fun pkgs).coq or "default"}.overrideScope'
         (coqPackages: super-coqPackages:
           let
@@ -47,8 +49,11 @@ let
                       if elem version [ "master" "cauchy_etoile" "holomorphy" ]
                       then {
                         propagatedBuildInputs = mca.propagatedBuildInputs ++
-                                                [coqPackages.mathcomp-real-closed];
-                      } else {});
+                                                [ coqPackages.mathcomp-real-closed coqPackages.hiearchy-builder ];
+                      } else {
+                        propagatedBuildInputs = mca.propagatedBuildInputs ++
+                                                (with coqPackages; [ coq-elpi hierarchy-builder ]);
+                      });
                 };
                 for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} =
                   (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) //
@@ -88,16 +93,38 @@ let
       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";
@@ -111,5 +138,12 @@ let
 in
 if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: {
   inherit shellHook mathcompnix;
-  buildInputs = (old.buildInputs or []) ++ pkgs.lib.optional withEmacs emacs;
+
+  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
diff --git a/opam b/opam
@@ -22,6 +22,7 @@ depends: [
   "coq" { ((>= "8.10" & < "8.13~") | = "dev") }
   "coq-mathcomp-field"       {(>= "1.11.0" & < "1.12~")}
   "coq-mathcomp-finmap"      {(>= "1.5.0" & < "1.6~")}
+  "coq-hiearchy-builder"     {(>= "0.10.0" & < "0.11~")}
 ]
 synopsis: "An analysis library for mathematical components"
 description: """