|
1 | | -{ |
2 | | - nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix |
3 | | - else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/502845c3e31ef3de0e424f3fcb09217df2ce6df6.tar.gz), |
4 | | - config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}), |
5 | | - withEmacs ? false, |
6 | | - print-env ? false, |
7 | | - do-nothing ? false, |
8 | | - package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"), |
9 | | - src ? (if builtins.pathExists ./package.nix then ./. else false) |
10 | | -}: |
11 | | -with builtins; |
12 | | -let |
13 | | - cfg-fun = if isFunction config then config else (pkgs: config); |
14 | | - pkg-src = if src == false then {} |
15 | | - else { ${if package == "mathcomp.single" then "mathcomp" else package} = src; }; |
16 | | - pkgs = if isAttrs nixpkgs then nixpkgs else import nixpkgs { |
17 | | - overlays = [ (pkgs: super-pkgs: with pkgs.lib; |
18 | | - let coqPackages = with pkgs; { |
19 | | - "8.7" = coqPackages_8_7; |
20 | | - "8.8" = coqPackages_8_8; |
21 | | - "8.9" = coqPackages_8_9; |
22 | | - "8.10" = coqPackages_8_10; |
23 | | - "8.11" = coqPackages_8_11; |
24 | | - "8.12" = coqPackages_8_12; |
25 | | - "default" = coqPackages_8_10; |
26 | | - }.${(cfg-fun pkgs).coq or "default"}.overrideScope' |
27 | | - (coqPackages: super-coqPackages: |
28 | | - let |
29 | | - all-pkgs = pkgs // { inherit coqPackages; }; |
30 | | - cfg = pkg-src // { |
31 | | - mathcomp-fast = { |
32 | | - src = ./.; |
33 | | - propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-fast); |
34 | | - }; |
35 | | - mathcomp-full = { |
36 | | - src = ./.; |
37 | | - propagatedBuildInputs = with coqPackages; ([ mathcomp ] ++ mathcomp-extra-all); |
38 | | - }; |
39 | | - } // (cfg-fun all-pkgs); |
40 | | - in { |
41 | | - mathcomp-extra-config = |
42 | | - let mec = super-coqPackages.mathcomp-extra-config; in |
43 | | - lib.recursiveUpdate mec { |
44 | | - initial = { |
45 | | - # fixing mathcomp analysis to depend on real-closed |
46 | | - mathcomp-analysis = {version, coqPackages} @ args: |
47 | | - let mca = mec.initial.mathcomp-analysis args; in |
48 | | - mca // { |
49 | | - propagatedBuildInputs = mca.propagatedBuildInputs ++ |
50 | | - (if builtins.elem coq.version ["8.10" "8.11" "8.12"] then (with coqPackages; [ coq-elpi hierarchy-builder ]) else []); |
51 | | - }; |
52 | | - }; |
53 | | - for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} = |
54 | | - (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) // |
55 | | - (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]); |
56 | | - }; |
57 | | - mathcomp = if cfg?mathcomp then coqPackages.mathcomp_ cfg.mathcomp else super-coqPackages.mathcomp; |
58 | | - } // mapAttrs |
59 | | - (package: version: coqPackages.mathcomp-extra package version) |
60 | | - (removeAttrs cfg ["mathcomp" "coq"]) |
61 | | - ); in { |
62 | | - coqPackages = coqPackages.filterPackages coqPackages.coq coqPackages; |
63 | | - coq = coqPackages.coq; |
64 | | - mc-clean = src: { |
65 | | - version = baseNameOf src; |
66 | | - src = cleanSourceWith { |
67 | | - src = cleanSource src; |
68 | | - filter = path: type: let baseName = baseNameOf (toString path); in ! ( |
69 | | - hasSuffix ".aux" baseName || |
70 | | - hasSuffix ".d" baseName || |
71 | | - hasSuffix ".vo" baseName || |
72 | | - hasSuffix ".glob" baseName || |
73 | | - elem baseName ["Makefile.coq" "Makefile.coq.conf" ".mailmap" ".git"] |
74 | | - ); |
75 | | - }; |
76 | | - }; |
77 | | - })]; |
78 | | - }; |
79 | | - |
80 | | - mathcompnix = ./.; |
81 | | - |
82 | | - shellHook = '' |
83 | | - nixEnv () { |
84 | | - echo "Here is your work environement" |
85 | | - echo "buildInputs:" |
86 | | - for x in $buildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done |
87 | | - echo "propagatedBuildInputs:" |
88 | | - for x in $propagatedBuildInputs; do printf " "; echo $x | cut -d "-" -f "2-"; done |
89 | | - 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" |
90 | | - } |
91 | | -
|
92 | | - printEnv () { |
93 | | - for x in $buildInputs; do echo $x; done |
94 | | - for x in $propagatedBuildInputs; do echo $x; done |
95 | | - } |
96 | | -
|
97 | | - cachixEnv () { |
98 | | - echo "Pushing environement to cachix" |
99 | | - printEnv | cachix push math-comp |
100 | | - } |
101 | | -
|
102 | | - nixDefault () { |
103 | | - cat $mathcompnix/default.nix |
104 | | - } > default.nix |
105 | | -
|
106 | | - updateNixPkgs (){ |
107 | | - HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1); |
108 | | - URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz |
109 | | - SHA256=$(nix-prefetch-url --unpack $URL) |
110 | | - echo "fetchTarball { |
111 | | - url = $URL; |
112 | | - sha256 = \"$SHA256\"; |
113 | | - }" > nixpkgs.nix |
114 | | - } |
115 | | - updateNixPkgsMaster (){ |
116 | | - HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1); |
117 | | - URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz |
118 | | - SHA256=$(nix-prefetch-url --unpack $URL) |
119 | | - echo "fetchTarball { |
120 | | - url = $URL; |
121 | | - sha256 = \"$SHA256\"; |
122 | | - }" > nixpkgs.nix |
123 | | - } |
124 | | - '' |
125 | | - + pkgs.lib.optionalString print-env "nixEnv"; |
126 | | - |
127 | | - emacs = with pkgs; emacsWithPackages |
128 | | - (epkgs: with epkgs.melpaStablePackages; [proof-general]); |
129 | | - |
130 | | - pkg = with pkgs; |
131 | | - if package == "mathcomp.single" then coqPackages.mathcomp.single |
132 | | - else coqPackages.${package} or (coqPackages.current-mathcomp-extra package); |
| 1 | +{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false, |
| 2 | + update-nixpkgs ? false, ci-matrix ? false, |
| 3 | + override ? {}, ocaml-override ? {}, global-override ? {}, |
| 4 | + bundle ? null, job ? null, inNixShell ? null, src ? ./., |
| 5 | +}@args: |
| 6 | +let auto = fetchGit { |
| 7 | + url = "https://github.com/coq-community/coq-nix-toolbox.git"; |
| 8 | + ref = "master"; |
| 9 | + rev = import .nix/coq-nix-toolbox.nix; |
| 10 | +}; |
133 | 11 | in |
134 | | -if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: { |
135 | | - inherit shellHook mathcompnix; |
136 | | - |
137 | | - buildInputs = if do-nothing then [] |
138 | | - else (old.buildInputs ++ |
139 | | - (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs |
140 | | - else [])); |
141 | | - |
142 | | - propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs; |
143 | | - |
144 | | -}) else pkg |
| 12 | +import auto ({inherit src;} // args) |
0 commit comments