diff options
| author | Cyril Cohen | 2021-03-12 10:18:31 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2021-03-12 13:51:10 +0100 |
| commit | 60d56f2bb32201be435b7cd4462dd778ed559aa4 (patch) | |
| tree | 8b914fdf342673f42c35f7dece3c58f9dbedb45a /default.nix | |
| parent | 476aa248bebcd2eb85b51b0b818dc37eaf94d6f2 (diff) | |
Use nix-tool-box
Diffstat (limited to 'default.nix')
| -rw-r--r-- | default.nix | 155 |
1 files changed, 12 insertions, 143 deletions
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 |
