tjh.dev
1{
2 lib,
3 pkgs,
4 mkCoqDerivation,
5 coq,
6 zchaff,
7 cvc5,
8 stdlib,
9 version ? null,
10}:
11
12# Broken since https://github.com/NixOS/nixpkgs/pull/354627, temporarily disactivated
13# let
14# # version of veriT that works with SMTCoq
15# veriT' = veriT.overrideAttrs (oA: {
16# src = fetchurl {
17# url = "https://www.lri.fr/~keller/Documents-recherche/Smtcoq/veriT9f48a98.tar.gz";
18# sha256 = "sha256-Pe46PxQVHWwWwx5Ei4Bl95A0otCiXZuUZ2nXuZPYnhY=";
19# };
20# meta.broken = false;
21# });
22# in
23
24mkCoqDerivation {
25 pname = "smtcoq";
26 owner = "smtcoq";
27
28 release."SMTCoq-2.2+8.19".sha256 = "sha256-9Wv8AXRRyOHG/cjA/V9tSK55R/bofDMLTkDpuwYWkks=";
29 release."SMTCoq-2.2+8.18".sha256 = "sha256-1iJAruI5Qn9nTZcUDjk8t/1Q+eFkYLOe9Ee0DmK03w8=";
30 release."SMTCoq-2.2+8.17".sha256 = "sha256-kaodsyVUl1+QQagzoBTIjxbdD4X3IaaH0x2AsVUL+Z0=";
31 release."SMTCoq-2.2+8.16".sha256 = "sha256-Hwm8IFlw97YiOY6H63HyJlwIXvQHr9lqc1+PgTnBtkw=";
32 release."SMTCoq-2.2+8.15".sha256 = "sha256-+GYOasJ32KJyOfqJlTtFmsJ2exd6gdueKwHdeMPErTo=";
33 release."SMTCoq-2.2+8.14".sha256 = "sha256-jqnF33E/4CqR1HSrLmUmLVCKslw9h3bbWi4YFmFYrhY=";
34 release."SMTCoq-2.2+8.13".sha256 = "sha256-AVpKU/SLaLYnCnx6GOEPGJjwbRrp28Fs5O50kJqdclI=";
35 release."SMTCoq-2.1+8.16".rev = "4996c00b455bfe98400e96c954839ceea93efdf7";
36 release."SMTCoq-2.1+8.16".sha256 = "sha256-k53e+frUjwq+ZZKbbOKd/EfVC40QeAzB2nCsGkCKnHA=";
37 release."SMTCoq-2.1+8.14".rev = "e11d9b424b0113f32265bcef0ddc962361da4dae";
38 release."SMTCoq-2.1+8.14".sha256 = "sha256-4a01/CRHUon2OfpagAnMaEVkBFipPX3MCVmSFS1Bnt4=";
39 release."SMTCoq-2.1+8.13".rev = "d02269c43739f4559d83873563ca00daad9faaf1";
40 release."SMTCoq-2.1+8.13".sha256 = "sha256-VZetGghdr5uJWDwZWSlhYScoNEoRHIbwqwJKSQyfKKg=";
41
42 releaseRev = v: v;
43
44 inherit version;
45 defaultVersion =
46 with lib.versions;
47 lib.switch coq.version [
48 {
49 case = isEq "8.19";
50 out = "SMTCoq-2.2+8.19";
51 }
52 {
53 case = isEq "8.18";
54 out = "SMTCoq-2.2+8.18";
55 }
56 {
57 case = isEq "8.17";
58 out = "SMTCoq-2.2+8.17";
59 }
60 {
61 case = isEq "8.16";
62 out = "SMTCoq-2.2+8.16";
63 }
64 {
65 case = isEq "8.15";
66 out = "SMTCoq-2.2+8.15";
67 }
68 {
69 case = isEq "8.14";
70 out = "SMTCoq-2.2+8.14";
71 }
72 {
73 case = isEq "8.13";
74 out = "SMTCoq-2.2+8.13";
75 }
76 ] null;
77
78 propagatedBuildInputs = [
79 cvc5
80 # veriT' # c.f. comment above
81 zchaff
82 stdlib
83 ]
84 ++ (with coq.ocamlPackages; [
85 findlib
86 num
87 zarith
88 ]);
89 mlPlugin = true;
90 nativeBuildInputs = (with pkgs; [ gnumake42 ]) ++ (with coq.ocamlPackages; [ ocamlbuild ]);
91
92 # This is meant to ease future troubleshooting of cvc5 build failures
93 passthru = { inherit cvc5; };
94
95 meta = with lib; {
96 description = "Communication between Coq and SAT/SMT solvers";
97 maintainers = with maintainers; [ siraben ];
98 license = licenses.cecill-b;
99 platforms = platforms.unix;
100 };
101}