tjh.dev
1{
2 coq,
3 mkCoqDerivation,
4 mathcomp,
5 coqeal,
6 mathcomp-real-closed,
7 mathcomp-bigenough,
8 mathcomp-zify,
9 mathcomp-algebra-tactics,
10 lib,
11 version ? null,
12}:
13
14mkCoqDerivation {
15
16 pname = "apery";
17
18 inherit version;
19 defaultVersion =
20 let
21 case = coq: mc: out: {
22 cases = [
23 coq
24 mc
25 ];
26 inherit out;
27 };
28 in
29 with lib.versions;
30 lib.switch
31 [ coq.coq-version mathcomp.version ]
32 [
33 (case (range "8.13" "8.16") (range "1.12.0" "1.17.0") "1.0.2")
34 ]
35 null;
36
37 release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
38
39 propagatedBuildInputs = [
40 mathcomp.field
41 coqeal
42 mathcomp-real-closed
43 mathcomp-bigenough
44 mathcomp-zify
45 mathcomp-algebra-tactics
46 ];
47
48 meta = {
49 description = "Formally verified proof in Coq, by computer algebra, that ζ(3) is irrational";
50 license = lib.licenses.cecill-c;
51 };
52}