pyrox.dev
1{ lib, fetchzip, mkCoqDerivation, coq, version ? null }:
2
3let
4 release = {
5 "8.18.0+0.18.0".sha256 = "sha256-c+3yG9vcbek/uvQ27OOQGqqsIHU1VuQhQvNVOjfucbo=";
6 "8.17.0+0.17.0".sha256 = "sha256-I81qvaXpJfXcbFw8vyzYLzlnhPg1QD0lTqAFXhoZ0rI=";
7 "8.16.0+0.16.3".sha256 = "sha256-22Kawp8jAsgyBTppwN5vmN7zEaB1QfPs0qKxd6x/7Uc=";
8 "8.15.0+0.15.0".sha256 = "1vh99ya2dq6a8xl2jrilgs0rpj4j227qx8zvzd2v5xylx0p4bbrp";
9 "8.14.0+0.14.0".sha256 = "1kh80yb791yl771qbqkvwhbhydfii23a7lql0jgifvllm2k8hd8d";
10 "8.13.0+0.13.0".sha256 = "0k69907xn4k61w4mkhwf8kh8drw9pijk9ynijsppihw98j8w38fy";
11 "8.12.0+0.12.1".sha256 = "048x3sgcq4h845hi6hm4j4dsfca8zfj70dm42w68n63qcm6xf9hn";
12 "8.11.0+0.11.1".sha256 = "1phmh99yqv71vlwklqgfxiq2vj99zrzxmryj2j4qvg5vav3y3y6c";
13 "8.10.0+0.7.2".sha256 = "1ljzm63hpd0ksvkyxcbh8rdf7p90vg91gb4h0zz0941v1zh40k8c";
14 };
15in
16
17(with lib; mkCoqDerivation {
18 pname = "serapi";
19 inherit version release;
20
21 defaultVersion = with versions;
22 lib.switch coq.version [
23 { case = isEq "8.18"; out = "8.18.0+0.18.0"; }
24 { case = isEq "8.17"; out = "8.17.0+0.17.0"; }
25 { case = isEq "8.16"; out = "8.16.0+0.16.3"; }
26 { case = isEq "8.15"; out = "8.15.0+0.15.0"; }
27 { case = isEq "8.14"; out = "8.14.0+0.14.0"; }
28 { case = isEq "8.13"; out = "8.13.0+0.13.0"; }
29 { case = isEq "8.12"; out = "8.12.0+0.12.1"; }
30 { case = isEq "8.11"; out = "8.11.0+0.11.1"; }
31 { case = isEq "8.10"; out = "8.10.0+0.7.2"; }
32 ] null;
33
34 useDune = true;
35
36 patches = [ ./janestreet-0.15.patch ];
37
38 propagatedBuildInputs =
39 with coq.ocamlPackages; [
40 cmdliner
41 findlib # run time dependency of SerAPI
42 ppx_deriving
43 ppx_deriving_yojson
44 ppx_import
45 ppx_sexp_conv
46 ppx_hash
47 sexplib
48 yojson
49 zarith # needed because of Coq
50 ];
51
52 installPhase = ''
53 runHook preInstall
54 dune install --prefix $out --libdir $OCAMLFIND_DESTDIR coq-serapi
55 runHook postInstall
56 '';
57
58 meta = with lib; {
59 homepage = "https://github.com/ejgallego/coq-serapi";
60 description = "SerAPI is a library for machine-to-machine interaction with the Coq proof assistant";
61 license = licenses.lgpl21Plus;
62 maintainers = with maintainers; [ alizter Zimmi48 ];
63 };
64}).overrideAttrs(o:
65 let inherit (o) version; in {
66 src = fetchzip {
67 url =
68 "https://github.com/ejgallego/coq-serapi/releases/download/${version}/coq-serapi-${
69 if version == "8.11.0+0.11.1" then version
70 else builtins.replaceStrings [ "+" ] [ "." ] version
71 }.tbz";
72 sha256 = release."${version}".sha256;
73 };
74
75 patches =
76 if version == "8.10.0+0.7.2"
77 then [
78 ./8.10.0+0.7.2.patch
79 ]
80 else if version == "8.11.0+0.11.1"
81 then [
82 ./8.11.0+0.11.1.patch
83 ]
84 else if version == "8.12.0+0.12.1" || version == "8.13.0+0.13.0"
85 then [
86 ./8.12.0+0.12.1.patch
87 ]
88 else if version == "8.14.0+0.14.0" || version == "8.15.0+0.15.0"
89 then [
90 ./janestreet-0.15.patch
91 ]
92 else if version == "8.16.0+0.16.3" || version == "8.17.0+0.17.0"
93 then [
94 ./janestreet-0.16.patch
95 ]
96 else [
97 ];
98
99 propagatedBuildInputs = o.propagatedBuildInputs ++
100 lib.optional (version == "8.16.0+0.16.3" || version == "dev") coq.ocamlPackages.ppx_hash
101 ;
102
103})