pyrox.dev
1{
2 coq,
3 mkCoqDerivation,
4 mathcomp,
5 mathcomp-bigenough,
6 lib,
7 version ? null,
8}:
9
10mkCoqDerivation {
11
12 namePrefix = [
13 "coq"
14 "mathcomp"
15 ];
16 pname = "real-closed";
17 owner = "math-comp";
18 inherit version;
19 release = {
20 "2.0.3".sha256 = "sha256-heZ7aZ7TO9YNAESIvbAc1qqzO91xMyLAox8VKueIk/s=";
21 "2.0.2".sha256 = "sha256-hBo9JMtmXDYBmf5ihKGksQLHv3c0+zDBnd8/aI2V/ao=";
22 "2.0.1".sha256 = "sha256-tQTI3PCl0q1vWpps28oATlzOI8TpVQh1jhTwVmhaZic=";
23 "2.0.0".sha256 = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8=";
24 "1.1.4".sha256 = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4=";
25 "1.1.3".sha256 = "1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7";
26 "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
27 "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
28 "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
29 "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
30 "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
31 "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
32 };
33
34 defaultVersion =
35 let
36 case = coq: mc: out: {
37 cases = [
38 coq
39 mc
40 ];
41 inherit out;
42 };
43 in
44 with lib.versions;
45 lib.switch
46 [ coq.version mathcomp.version ]
47 [
48 (case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3")
49 (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2")
50 (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1")
51 (case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0")
52 (case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4")
53 (case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3")
54 (case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2")
55 (case (isGe "8.7") "1.11.0" "1.1.1")
56 (case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4")
57 (case (isGe "8.7") "1.8.0" "1.0.3")
58 (case (isGe "8.7") "1.7.0" "1.0.1")
59 ]
60 null;
61
62 propagatedBuildInputs = [
63 mathcomp.ssreflect
64 mathcomp.algebra
65 mathcomp.field
66 mathcomp.fingroup
67 mathcomp.solvable
68 mathcomp-bigenough
69 ];
70
71 meta = {
72 description = "Mathematical Components Library on real closed fields";
73 license = lib.licenses.cecill-c;
74 };
75}