blob: 195a47e4f59e4f17d26146406c1c38a8c3a1e810 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
{
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
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
|
