From 9b1e649d78a11b256bc55eb90f801206a63608d1 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sat, 23 May 2020 03:34:20 +0200 Subject: [PATCH] upgrading default.nix --- config.nix | 4 ++++ default.nix | 61 +++++++++++++++++++++++++++++++++++------------------ package.nix | 1 + 3 files changed, 46 insertions(+), 20 deletions(-) create mode 100644 config.nix create mode 100644 package.nix diff --git a/config.nix b/config.nix new file mode 100644 index 0000000000..afc2ea79ac --- /dev/null +++ b/config.nix @@ -0,0 +1,4 @@ +{ + coq = "8.10"; + mathcomp = "1.11.0+beta1"; +} diff --git a/default.nix b/default.nix index 20843850b3..82542c8dfc 100644 --- a/default.nix +++ b/default.nix @@ -1,14 +1,18 @@ { - nixpkgs ? (fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-1.11.tar.gz), - config ? (pkgs: {}), + nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix + else fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-fix-rec.tar.gz), + config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}), withEmacs ? false, print-env ? false, - package ? "mathcomp-analysis" + 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); - pkgs = import nixpkgs { + 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; @@ -18,25 +22,39 @@ let "8.11" = coqPackages_8_11; "default" = coqPackages_8_10; }.${(cfg-fun pkgs).coq or "default"}.overrideScope' - (self: super: + (coqPackages: super-coqPackages: let - all-pkgs = pkgs // { coqPackages = self; }; - cfg = { ${package} = ./.; } // { + all-pkgs = pkgs // { inherit coqPackages; }; + cfg = pkg-src // { mathcomp-fast = { src = ./.; - propagatedBuildInputs = with self; ([ mathcomp ] ++ mathcomp-extra-fast); + propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast); }; mathcomp-full = { src = ./.; - propagatedBuildInputs = with self; ([ mathcomp ] ++ mathcomp-extra-all); + propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all); }; } // (cfg-fun all-pkgs); in { - # mathcomp-extra-config = lib.recursiveUpdate super.mathcomp-extra-config { - # for-coq-and-mc.${self.coq.coq-version}.${self.mathcomp.version} = - # removeAttrs cfg ["mathcomp" "coq"]; - # }; - mathcomp = if cfg?mathcomp then self.mathcomp_ cfg.mathcomp else super.mathcomp_ "1.11.0+beta1"; + 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 // ( + if elem version [ "master" "cauchy_etoile" "holomorphy" ] + then { + propagatedBuildInputs = mca.propagatedBuildInputs ++ + [coqPackages.mathcomp-real-closed]; + } 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"]) @@ -48,13 +66,11 @@ let src = cleanSourceWith { src = cleanSource src; filter = path: type: let baseName = baseNameOf (toString path); in ! ( - # Filter out editor backup / swap files. - hasPrefix ".git" baseName || hasSuffix ".aux" baseName || hasSuffix ".d" baseName || hasSuffix ".vo" baseName || hasSuffix ".glob" baseName || - elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap"] + elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"] ); }; }; @@ -72,10 +88,13 @@ 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" - for x in $buildInputs; do printf " "; echo $x | cachix push math-comp; done - for x in $propagatedBuildInputs; do printf " "; echo $x | cachix push math-comp; done + printEnv | cachix push math-comp } nixDefault () { cat $mathcompnix/default.nix @@ -86,7 +105,9 @@ let emacs = with pkgs; emacsWithPackages (epkgs: with epkgs.melpaStablePackages; [proof-general]); - pkg = with pkgs; coqPackages.${package} or (coqPackages.current-mathcomp-extra package); + pkg = with pkgs; + if package == "mathcomp.single" then coqPackages.mathcomp.single + else coqPackages.${package} or (coqPackages.current-mathcomp-extra package); in if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: { inherit shellHook mathcompnix; diff --git a/package.nix b/package.nix new file mode 100644 index 0000000000..e8e708431a --- /dev/null +++ b/package.nix @@ -0,0 +1 @@ +"mathcomp-analysis"