diff options
Diffstat (limited to 'default.nix')
| -rw-r--r-- | default.nix | 155 |
1 files changed, 143 insertions, 12 deletions
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 |