tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp-boot,
6 mathcomp-fingroup,
7 mathcomp-algebra,
8 stdlib,
9 version ? null,
10}:
11
12mkCoqDerivation {
13 namePrefix = [
14 "coq"
15 "mathcomp"
16 ];
17 pname = "zify";
18 repo = "mczify";
19 owner = "math-comp";
20 inherit version;
21
22 defaultVersion =
23 let
24 case = coq: mc: out: {
25 cases = [
26 coq
27 mc
28 ];
29 inherit out;
30 };
31 in
32 with lib.versions;
33 lib.switch
34 [ coq.coq-version mathcomp-algebra.version ]
35 [
36 (case (range "8.16" "9.1") (isGe "2.0.0") "1.5.0+2.0+8.16")
37 (case (range "8.13" "8.20") (range "1.12" "1.19.0") "1.3.0+1.12+8.13")
38 (case (range "8.13" "8.16") (range "1.12" "1.17.0") "1.1.0+1.12+8.13")
39 ]
40 null;
41
42 release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
43 release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";
44 release."1.3.0+1.12+8.13".sha256 = "sha256-ebfY8HatP4te44M6o84DSLpDCkMu4IroPCy+HqzOnTE=";
45 release."1.5.0+2.0+8.16".sha256 = "sha256-boBYGvXdGFc6aPnjgSZYSoW4kmN5khtNrSV3DUv9DqM=";
46
47 propagatedBuildInputs = [
48 mathcomp-boot
49 mathcomp-algebra
50 mathcomp-fingroup
51 stdlib
52 ];
53
54 meta = {
55 description = "Micromega tactics for Mathematical Components";
56 maintainers = with lib.maintainers; [ cohencyril ];
57 };
58}