tangled
alpha
login
or
join now
pyrox.dev
/
nixpkgs
0
fork
atom
lol
0
fork
atom
overview
issues
pulls
pipelines
coq: init at 8.8+beta1
Vincent Laporte
8 years ago
6845b248
13e74a83
+67
-18
16 changed files
expand all
collapse all
unified
split
pkgs
applications
science
logic
coq
default.nix
development
coq-modules
CoLoR
default.nix
QuickChick
default.nix
autosubst
default.nix
bignums
default.nix
coq-ext-lib
default.nix
coq-haskell
default.nix
coquelicot
default.nix
dpdgraph
default.nix
heq
default.nix
interval
default.nix
mathcomp
generic.nix
paco
default.nix
ssreflect
generic.nix
top-level
all-packages.nix
coq-packages.nix
+3
-3
pkgs/applications/science/logic/coq/default.nix
reviewed
···
22
22
"8.7.0" = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m";
23
23
"8.7.1" = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8";
24
24
"8.7.2" = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w";
25
25
+
"8.8+beta1" = "19ipmx6bf8wjpk8y29hcginxk7hps4jh1bbihn5icx4qysm81165";
25
26
}."${version}";
26
27
coq-version = builtins.substring 0 3 version;
27
28
camlp5 = ocamlPackages.camlp5_strict;
···
37
38
inherit camlp5;
38
39
inherit (ocamlPackages) ocaml;
39
40
passthru = {
40
40
-
inherit (ocamlPackages) findlib;
41
41
+
inherit (ocamlPackages) findlib num;
41
42
emacsBufferSetup = pkgs: ''
42
43
; Propagate coq paths to children
43
44
(inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
···
92
93
};
93
94
94
95
nativeBuildInputs = [ pkgconfig ];
95
95
-
buildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib camlp5 ncurses ]
96
96
+
buildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib camlp5 ncurses ocamlPackages.num ]
96
97
++ stdenv.lib.optional buildIde ocamlPackages.lablgtk;
97
98
98
99
postPatch = ''
···
116
117
117
118
preConfigure = ''
118
119
configureFlagsArray=(
119
119
-
-opt
120
120
${ideFlags}
121
121
)
122
122
'';
+1
-1
pkgs/development/coq-modules/CoLoR/default.nix
reviewed
···
23
23
};
24
24
25
25
passthru = {
26
26
-
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
26
26
+
compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ];
27
27
};
28
28
}
+8
-4
pkgs/development/coq-modules/QuickChick/default.nix
reviewed
···
1
1
{ stdenv, fetchFromGitHub, coq, ssreflect }:
2
2
3
3
-
let param =
3
3
+
let params =
4
4
{
5
5
"8.5" = {
6
6
version = "20170512";
···
19
19
rev = "195e550a1cf0810497734356437a1720ebb6d744";
20
20
sha256 = "0zm23y89z0h4iamy74qk9qi2pz2cj3ga6ygav0w79n0qyqwhxcq1";
21
21
};
22
22
-
23
23
-
}."${coq.coq-version}"
24
24
-
; in
22
22
+
};
23
23
+
param = params."${coq.coq-version}";
24
24
+
in
25
25
26
26
stdenv.mkDerivation rec {
27
27
···
47
47
description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck";
48
48
maintainers = with maintainers; [ jwiegley ];
49
49
platforms = coq.meta.platforms;
50
50
+
};
51
51
+
52
52
+
passthru = {
53
53
+
compatibleCoqVersions = v: builtins.hasAttr v params;
50
54
};
51
55
52
56
}
+2
pkgs/development/coq-modules/autosubst/default.nix
reviewed
···
24
24
platforms = coq.meta.platforms;
25
25
};
26
26
27
27
+
passthru = { inherit (mathcomp) compatibleCoqVersions; };
28
28
+
27
29
}
+4
pkgs/development/coq-modules/bignums/default.nix
reviewed
···
10
10
rev = "V8.7.0";
11
11
sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
12
12
};
13
13
+
"8.8" = {
14
14
+
rev = "V8.8+beta1";
15
15
+
sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
16
16
+
};
13
17
}."${coq.coq-version}"
14
18
; in
15
19
+6
-2
pkgs/development/coq-modules/coq-ext-lib/default.nix
reviewed
···
1
1
{ stdenv, fetchFromGitHub, coq }:
2
2
3
3
-
let param =
3
3
+
let params =
4
4
{
5
5
"8.5" = { version = "0.9.4"; sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; };
6
6
"8.6" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; };
7
7
"8.7" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; };
8
8
-
}."${coq.coq-version}";
8
8
+
};
9
9
+
param = params."${coq.coq-version}";
9
10
in
10
11
11
12
stdenv.mkDerivation rec {
···
34
35
platforms = coq.meta.platforms;
35
36
};
36
37
38
38
+
passthru = {
39
39
+
compatibleCoqVersions = v: builtins.hasAttr v params;
40
40
+
};
37
41
}
+7
-4
pkgs/development/coq-modules/coq-haskell/default.nix
reviewed
···
1
1
{ stdenv, fetchgit, coq, ssreflect }:
2
2
3
3
-
let param =
3
3
+
let params =
4
4
{
5
5
"8.5" = {
6
6
version = "20171215";
···
19
19
rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
20
20
sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
21
21
};
22
22
-
23
23
-
}."${coq.coq-version}"
24
24
-
; in
22
22
+
};
23
23
+
param = params."${coq.coq-version}";
24
24
+
in
25
25
26
26
stdenv.mkDerivation rec {
27
27
···
48
48
platforms = coq.meta.platforms;
49
49
};
50
50
51
51
+
passthru = {
52
52
+
compatibleCoqVersions = v: builtins.hasAttr v params;
53
53
+
};
51
54
}
+3
pkgs/development/coq-modules/coquelicot/default.nix
reviewed
···
22
22
maintainers = [ stdenv.lib.maintainers.vbgl ];
23
23
inherit (coq.meta) platforms;
24
24
};
25
25
+
26
26
+
passthru = { inherit (ssreflect) compatibleCoqVersions; };
27
27
+
25
28
}
+9
-2
pkgs/development/coq-modules/dpdgraph/default.nix
reviewed
···
1
1
{ stdenv, fetchFromGitHub, autoreconfHook, coq, ocamlPackages }:
2
2
3
3
-
let param = {
3
3
+
let params = {
4
4
"8.7" = {
5
5
version = "0.6.2";
6
6
rev = "d76ddde37d918569945774733b7997e8b24daf51";
···
16
16
rev = "v0.6";
17
17
sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
18
18
};
19
19
-
}."${coq.coq-version}"; in
19
19
+
};
20
20
+
param = params."${coq.coq-version}";
21
21
+
in
20
22
21
23
stdenv.mkDerivation {
22
24
name = "coq${coq.coq-version}-dpdgraph-${param.version}";
···
46
48
maintainers = with stdenv.lib.maintainers; [ vbgl ];
47
49
platforms = coq.meta.platforms;
48
50
};
51
51
+
52
52
+
passthru = {
53
53
+
compatibleCoqVersions = v: builtins.hasAttr v params;
54
54
+
};
55
55
+
49
56
}
+3
pkgs/development/coq-modules/heq/default.nix
reviewed
···
24
24
platforms = coq.meta.platforms;
25
25
};
26
26
27
27
+
passthru = {
28
28
+
compatibleCoqVersions = v: !stdenv.lib.versionAtLeast v "8.8";
29
29
+
};
27
30
}
+3
pkgs/development/coq-modules/interval/default.nix
reviewed
···
24
24
maintainers = with maintainers; [ vbgl ];
25
25
platforms = coq.meta.platforms;
26
26
};
27
27
+
28
28
+
passthru = { inherit (mathcomp) compatibleCoqVersions; };
29
29
+
27
30
}
+4
pkgs/development/coq-modules/mathcomp/generic.nix
reviewed
···
35
35
platforms = coq.meta.platforms;
36
36
};
37
37
38
38
+
passthru = {
39
39
+
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
40
40
+
};
41
41
+
38
42
}
+4
pkgs/development/coq-modules/paco/default.nix
reviewed
···
28
28
platforms = coq.meta.platforms;
29
29
};
30
30
31
31
+
passthru = {
32
32
+
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
33
33
+
};
34
34
+
31
35
}
+4
pkgs/development/coq-modules/ssreflect/generic.nix
reviewed
···
42
42
platforms = coq.meta.platforms;
43
43
};
44
44
45
45
+
passthru = {
46
46
+
compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
47
47
+
};
48
48
+
45
49
}
+2
-2
pkgs/top-level/all-packages.nix
reviewed
···
19727
19727
19728
19728
inherit (callPackage ./coq-packages.nix {})
19729
19729
mkCoqPackages
19730
19730
-
coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7
19731
19731
-
coqPackages_8_5 coqPackages_8_6 coqPackages_8_7
19730
19730
+
coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7 coq_8_8
19731
19731
+
coqPackages_8_5 coqPackages_8_6 coqPackages_8_7 coqPackages_8_8
19732
19732
coqPackages coq
19733
19733
;
19734
19734
+4
pkgs/top-level/coq-packages.nix
reviewed
···
71
71
coq_8_7 = callPackage ../applications/science/logic/coq {
72
72
version = "8.7.2";
73
73
};
74
74
+
coq_8_8 = callPackage ../applications/science/logic/coq {
75
75
+
version = "8.8+beta1";
76
76
+
};
74
77
75
78
coqPackages_8_5 = mkCoqPackages coq_8_5;
76
79
coqPackages_8_6 = mkCoqPackages coq_8_6;
77
80
coqPackages_8_7 = mkCoqPackages coq_8_7;
81
81
+
coqPackages_8_8 = mkCoqPackages coq_8_8;
78
82
coqPackages = coqPackages_8_7;
79
83
coq = coqPackages.coq;
80
84