tjh.dev
1{
2 lib,
3 fetchzip,
4 mkCoqDerivation,
5 coq,
6 coq-lsp,
7 version ? null,
8}:
9
10let
11 release = {
12 "8.20.0+0.20.0".sha256 = "sha256-Mll3m7CVfh52yA5zACDzMZk8lwhOONMMliqQ2l/ObKI=";
13 "8.19.0+0.19.3".sha256 = "sha256-QWRXBTcjtAGskZBeLIuX7WDE95KfH6SxV8MJSMx8B2Q=";
14 "8.18.0+0.18.3".sha256 = "sha256-3JGZCyn62LYJVpfXiwnSMxvdA2vQNTL7li2ZBPcjF0M=";
15 "8.17.0+0.17.3".sha256 = "sha256-XolzpJd8zs4LLyJO4eWvCiAJ0HJSGBJTGVSBClQRGnw=";
16 "8.16.0+0.16.3".sha256 = "sha256-22Kawp8jAsgyBTppwN5vmN7zEaB1QfPs0qKxd6x/7Uc=";
17 "8.15.0+0.15.0".sha256 = "1vh99ya2dq6a8xl2jrilgs0rpj4j227qx8zvzd2v5xylx0p4bbrp";
18 "8.14.0+0.14.0".sha256 = "1kh80yb791yl771qbqkvwhbhydfii23a7lql0jgifvllm2k8hd8d";
19 "8.13.0+0.13.0".sha256 = "0k69907xn4k61w4mkhwf8kh8drw9pijk9ynijsppihw98j8w38fy";
20 "8.12.0+0.12.1".sha256 = "048x3sgcq4h845hi6hm4j4dsfca8zfj70dm42w68n63qcm6xf9hn";
21 "8.11.0+0.11.1".sha256 = "1phmh99yqv71vlwklqgfxiq2vj99zrzxmryj2j4qvg5vav3y3y6c";
22 "8.10.0+0.7.2".sha256 = "1ljzm63hpd0ksvkyxcbh8rdf7p90vg91gb4h0zz0941v1zh40k8c";
23 };
24in
25
26(mkCoqDerivation {
27 pname = "serapi";
28 owner = "ejgallego";
29 repo = "coq-serapi";
30 inherit version release;
31
32 defaultVersion = lib.switch coq.version [
33 {
34 case = lib.versions.isEq "8.20";
35 out = "8.20.0+0.20.0";
36 }
37 {
38 case = lib.versions.isEq "8.19";
39 out = "8.19.0+0.19.3";
40 }
41 {
42 case = lib.versions.isEq "8.18";
43 out = "8.18.0+0.18.3";
44 }
45 {
46 case = lib.versions.isEq "8.17";
47 out = "8.17.0+0.17.3";
48 }
49 {
50 case = lib.versions.isEq "8.16";
51 out = "8.16.0+0.16.3";
52 }
53 {
54 case = lib.versions.isEq "8.15";
55 out = "8.15.0+0.15.0";
56 }
57 {
58 case = lib.versions.isEq "8.14";
59 out = "8.14.0+0.14.0";
60 }
61 {
62 case = lib.versions.isEq "8.13";
63 out = "8.13.0+0.13.0";
64 }
65 {
66 case = lib.versions.isEq "8.12";
67 out = "8.12.0+0.12.1";
68 }
69 {
70 case = lib.versions.isEq "8.11";
71 out = "8.11.0+0.11.1";
72 }
73 {
74 case = lib.versions.isEq "8.10";
75 out = "8.10.0+0.7.2";
76 }
77 ] null;
78
79 useDune = true;
80
81 propagatedBuildInputs = with coq.ocamlPackages; [
82 cmdliner
83 findlib # run time dependency of SerAPI
84 ppx_sexp_conv
85 ppx_hash
86 sexplib
87 ];
88
89 installPhase = ''
90 runHook preInstall
91 dune install --prefix $out --libdir $OCAMLFIND_DESTDIR coq-serapi
92 runHook postInstall
93 '';
94
95 meta = with lib; {
96 homepage = "https://github.com/ejgallego/coq-serapi";
97 description = "SerAPI is a library for machine-to-machine interaction with the Coq proof assistant";
98 license = licenses.lgpl21Plus;
99 maintainers = with maintainers; [
100 alizter
101 Zimmi48
102 ];
103 };
104}).overrideAttrs
105 (
106 o:
107 if lib.versions.isLe "8.19.0+0.19.3" o.version && o.version != "dev" then
108 let
109 ppx_deriving = coq.ocamlPackages.ppx_deriving.override { version = "5.2.1"; };
110 in
111 let
112 inherit (o) version;
113 in
114 {
115 src = fetchzip {
116 url = "https://github.com/ejgallego/coq-serapi/releases/download/${version}/coq-serapi-${
117 if version == "8.11.0+0.11.1" then version else builtins.replaceStrings [ "+" ] [ "." ] version
118 }.tbz";
119 sha256 = release."${version}".sha256;
120 };
121
122 patches =
123 lib.optional (lib.versions.isGe "8.16" version) ./sertop.patch
124 ++ (
125 if version == "8.10.0+0.7.2" then
126 [
127 ./8.10.0+0.7.2.patch
128 ]
129 else if version == "8.11.0+0.11.1" then
130 [
131 ./8.11.0+0.11.1.patch
132 ]
133 else if version == "8.12.0+0.12.1" || version == "8.13.0+0.13.0" then
134 [
135 ./8.12.0+0.12.1.patch
136 ]
137 else if version == "8.14.0+0.14.0" || version == "8.15.0+0.15.0" then
138 [
139 ./janestreet-0.15.patch
140 ]
141 else if version == "8.16.0+0.16.3" || version == "8.17.0+0.17.0" then
142 [
143 ./janestreet-0.16.patch
144 ]
145 else
146 [
147 ]
148 );
149
150 propagatedBuildInputs =
151 o.propagatedBuildInputs
152 ++ (with coq.ocamlPackages; [
153 ppx_deriving
154 (ppx_deriving_yojson.override { inherit ppx_deriving; })
155 (ppx_import.override { inherit ppx_deriving; })
156 yojson
157 zarith # zarith needed because of Coq
158 ]);
159 }
160 else
161 { propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq-lsp ]; }
162 )