tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
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.18" "9.1") (isGe "2.3.0") "1.6.0+2.3+8.18")
37 (case (range "8.16" "9.1") (isGe "2.0.0") "1.5.0+2.0+8.16")
38 (case (range "8.13" "8.20") (range "1.12" "1.19.0") "1.3.0+1.12+8.13")
39 (case (range "8.13" "8.16") (range "1.12" "1.17.0") "1.1.0+1.12+8.13")
40 ]
41 null;
42
43 release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
44 release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";
45 release."1.3.0+1.12+8.13".sha256 = "sha256-ebfY8HatP4te44M6o84DSLpDCkMu4IroPCy+HqzOnTE=";
46 release."1.5.0+2.0+8.16".sha256 = "sha256-boBYGvXdGFc6aPnjgSZYSoW4kmN5khtNrSV3DUv9DqM=";
47 release."1.6.0+2.3+8.18".sha256 = "sha256-rI5ZWtgO0a2sxCVChTdASxWxhgYEbM4OhC0dnSMRzZ8=";
48
49 propagatedBuildInputs = [
50 mathcomp-boot
51 mathcomp-algebra
52 mathcomp-fingroup
53 stdlib
54 ];
55
56 meta = {
57 description = "Micromega tactics for Mathematical Components";
58 maintainers = with lib.maintainers; [ cohencyril ];
59 };
60}