aboutsummaryrefslogtreecommitdiff
path: root/default.nix
diff options
context:
space:
mode:
Diffstat (limited to 'default.nix')
-rw-r--r--default.nix155
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