tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp-ssreflect,
6 mathcomp-algebra,
7 coq-elpi,
8 mathcomp-zify,
9 version ? null,
10}:
11
12mkCoqDerivation {
13 namePrefix = [
14 "coq"
15 "mathcomp"
16 ];
17 pname = "algebra-tactics";
18 owner = "math-comp";
19 inherit version;
20
21 defaultVersion =
22 let
23 case = coq: mc: out: {
24 cases = [
25 coq
26 mc
27 ];
28 inherit out;
29 };
30 in
31 with lib.versions;
32 lib.switch
33 [ coq.coq-version mathcomp-algebra.version ]
34 [
35 (case (range "8.20" "9.1") (isGe "2.4") "1.2.7")
36 (case (range "8.20" "9.1") (isGe "2.4") "1.2.6")
37 (case (range "8.20" "9.1") (isGe "2.4") "1.2.5")
38 (case (range "8.16" "9.0") (isGe "2.0") "1.2.4")
39 (case (range "8.16" "8.18") (isGe "2.0") "1.2.2")
40 (case (range "8.16" "8.19") (isGe "1.15") "1.1.1")
41 (case (range "8.13" "8.16") (isGe "1.12") "1.0.0")
42 ]
43 null;
44
45 release."1.0.0".sha256 = "sha256-kszARPBizWbxSQ/Iqpf2vLbxYc6AjpUCLnSNlPcNfls=";
46 release."1.1.1".sha256 = "sha256-5wItMeeTRoJlRBH3zBNc2VUZn6pkDde60YAvXTx+J3U=";
47 release."1.2.2".sha256 = "sha256-EU9RJGV3BvnmsX+mGH+6+MDXiGHgDI7aP5sIYiMUXTs=";
48 release."1.2.3".sha256 = "sha256-6uc1VEfDv+fExEfBR2c0/Q/KjrkX0TbEMCLgeYcpkls=";
49 release."1.2.4".sha256 = "sha256-BRxt0LGPz2u3kJRjcderaZqCfs8M8qKAAwNSWmIck7Q=";
50 release."1.2.5".sha256 = "sha256-wTfe+g7ljWs1S+g02VQutnJGLVIOzNX1lm1HTMXeUUA=";
51 release."1.2.6".sha256 = "sha256-D7EEiLeCJMgxsYvlAFyL7QZyx/KJAKesVE+vyfzqzkU=";
52 release."1.2.7".sha256 = "sha256-pCal3BPZ85SMAsEFAXRWWV7nuriHGWtyfNocJqsEmLk=";
53
54 propagatedBuildInputs = [
55 mathcomp-ssreflect
56 mathcomp-algebra
57 coq-elpi
58 mathcomp-zify
59 ];
60
61 meta = {
62 description = "Ring and field tactics for Mathematical Components";
63 maintainers = with lib.maintainers; [ cohencyril ];
64 };
65}