ocaml.scm
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2017 Julien Lepiller <julien@lepiller.eu> |
3 | ;;; |
4 | ;;; This file is part of GNU Guix. |
5 | ;;; |
6 | ;;; GNU Guix is free software; you can redistribute it and/or modify it |
7 | ;;; under the terms of the GNU General Public License as published by |
8 | ;;; the Free Software Foundation; either version 3 of the License, or (at |
9 | ;;; your option) any later version. |
10 | ;;; |
11 | ;;; GNU Guix is distributed in the hope that it will be useful, but |
12 | ;;; WITHOUT ANY WARRANTY; without even the implied warranty of |
13 | ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
14 | ;;; GNU General Public License for more details. |
15 | ;;; |
16 | ;;; You should have received a copy of the GNU General Public License |
17 | ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. |
18 | |
19 | (define-module (more packages ocaml) |
20 | #:use-module (guix packages) |
21 | #:use-module (guix download) |
22 | #:use-module (guix utils) |
23 | #:use-module (guix build-system gnu) |
24 | #:use-module (guix build-system ocaml) |
25 | #:use-module ((guix licenses) #:prefix license:) |
26 | #:use-module (gnu packages) |
27 | #:use-module (gnu packages base) |
28 | #:use-module (gnu packages bison) |
29 | #:use-module (gnu packages boost) |
30 | #:use-module (gnu packages emacs) |
31 | #:use-module (gnu packages flex) |
32 | #:use-module (gnu packages llvm) |
33 | #:use-module (gnu packages multiprecision) |
34 | #:use-module (gnu packages ocaml) |
35 | #:use-module (gnu packages perl) |
36 | #:use-module (gnu packages protobuf) |
37 | #:use-module (gnu packages texinfo)) |
38 | |
39 | ;; Janestreet packages are found in a similar way and all need the same patch. |
40 | (define (janestreet-origin name version hash) |
41 | (origin (method url-fetch) |
42 | (uri (string-append "https://ocaml.janestreet.com/ocaml-core/" |
43 | (version-major+minor version) "/files/" |
44 | name "-" version ".tar.gz")) |
45 | (sha256 (base32 hash)) |
46 | (modules '((guix build utils))) |
47 | (snippet |
48 | (let ((pattern (string-append "lib/" name))) |
49 | `(begin |
50 | ;; install.ml contains an invalid reference to the ppx file and |
51 | ;; propagates this error to the generated META file. It |
52 | ;; looks for it in the "lib" directory, but it is installed in |
53 | ;; "lib/ocaml/site-lib/package". This substitute does not change |
54 | ;; this file for non ppx packages. |
55 | (substitute* "install.ml" |
56 | ((,pattern) (string-append "lib/ocaml/site-lib/" ,name))) |
57 | ;; The standard Makefile would try to install janestreet modules |
58 | ;; in OCaml's directory in the store, which is read-only. |
59 | (substitute* "Makefile" |
60 | (("--prefix") |
61 | "--libdir $(LIBDIR) --prefix"))))))) |
62 | |
63 | ;; They also require almost the same set of arguments |
64 | (define janestreet-arguments |
65 | `(#:use-make? #t |
66 | #:make-flags |
67 | (list (string-append "CONFIGUREFLAGS=--prefix " |
68 | (assoc-ref %outputs "out") |
69 | " --enable-tests") |
70 | (string-append "LIBDIR=" |
71 | (assoc-ref %outputs "out") |
72 | "/lib/ocaml/site-lib") |
73 | ;; for ocaml-bin-prot, otherwise ignored |
74 | (string-append "OCAML_TOPLEVEL_PATH=" |
75 | (assoc-ref %build-inputs "findlib") |
76 | "/lib/ocaml/site-lib")) |
77 | #:phases (modify-phases %standard-phases (delete 'configure)))) |
78 | |
79 | (define-public ocaml-core-kernel |
80 | (package |
81 | (name "ocaml-core-kernel") |
82 | (version "113.33.03") |
83 | (source (janestreet-origin "core_kernel" version |
84 | "0fl23jrwivixawhxinbwaw9cabqnzn7fini7dxpxjjvkxdc8ip5y")) |
85 | (native-inputs |
86 | `(("js-build-tools" ,ocaml-js-build-tools) |
87 | ("ppx-jane" ,ocaml-ppx-jane) |
88 | ("opam" ,opam))) |
89 | (propagated-inputs |
90 | `(("bin_prot" ,ocaml-bin-prot) |
91 | ("ppx-assert" ,ocaml-ppx-assert) |
92 | ("ppx-bench" ,ocaml-ppx-bench) |
93 | ("ppx-driver" ,ocaml-ppx-driver) |
94 | ("ppx-expect" ,ocaml-ppx-expect) |
95 | ("ppx-inline-test" ,ocaml-ppx-inline-test) |
96 | ("typerep" ,ocaml-typerep) |
97 | ("sexplib" ,ocaml-sexplib) |
98 | ("variantslib" ,ocaml-variantslib) |
99 | ("result" ,ocaml-result) |
100 | ("fieldslib" ,ocaml-fieldslib))) |
101 | (build-system ocaml-build-system) |
102 | (arguments janestreet-arguments) |
103 | (home-page "https://github.com/janestreet/core_kernel/") |
104 | (synopsis "Portable standard library for OCaml") |
105 | (description "Core is an alternative to the OCaml standard library. |
106 | |
107 | Core_kernel is the system-independent part of Core. It is aimed for cases when |
108 | the full Core is not available, such as in Javascript.") |
109 | (license license:asl2.0))) |
110 | |
111 | (define-public ocaml-async-kernel |
112 | (package |
113 | (name "ocaml-async-kernel") |
114 | (version "113.33.03") |
115 | (source (janestreet-origin "async_kernel" version |
116 | "04bjsaa23j831r09r38x6xx9nhryvp0z5ihickvhxqa4fb2snyvd")) |
117 | (native-inputs |
118 | `(("oasis" ,ocaml-oasis) |
119 | ("js-build-tools" ,ocaml-js-build-tools) |
120 | ("ppx-jane" ,ocaml-ppx-jane) |
121 | ("opam" ,opam))) |
122 | (propagated-inputs |
123 | `(("core-kernel" ,ocaml-core-kernel))) |
124 | (build-system ocaml-build-system) |
125 | (arguments janestreet-arguments) |
126 | (home-page "https://github.com/janestreet/async_kernel/") |
127 | (synopsis "Monadic concurrency library") |
128 | (description "Monadic concurrency library.") |
129 | (license license:asl2.0))) |
130 | |
131 | (define-public ocaml-async-rpc-kernel |
132 | (package |
133 | (name "ocaml-async-rpc-kernel") |
134 | (version "113.33.03") |
135 | (source (janestreet-origin "async_rpc_kernel" version |
136 | "0y97h9pkb00v7jpf87m8cbb0ffkclj9g26ph6sq97q8dpisnkjwh")) |
137 | (native-inputs |
138 | `(("oasis" ,ocaml-oasis) |
139 | ("js-build-tools" ,ocaml-js-build-tools) |
140 | ("ppx-jane" ,ocaml-ppx-jane) |
141 | ("opam" ,opam))) |
142 | (propagated-inputs |
143 | `(("async-kernel" ,ocaml-async-kernel))) |
144 | (build-system ocaml-build-system) |
145 | (arguments janestreet-arguments) |
146 | (home-page "https://github.com/janestreet/async_rpc_kernel/") |
147 | (synopsis "Platform-independent core of Async RPC library") |
148 | (description "Platform-independent core of Async RPC library.") |
149 | (license license:asl2.0))) |
150 | |
151 | (define-public ocaml-core |
152 | (package |
153 | (name "ocaml-core") |
154 | (version "113.33.03") |
155 | (source (janestreet-origin "core" version |
156 | "1znll157qg56g9d3247fjibv1hxv3r9wxgr4nhy19j2vzdh6a268")) |
157 | (native-inputs |
158 | `(("oasis" ,ocaml-oasis) |
159 | ("js-build-tools" ,ocaml-js-build-tools) |
160 | ("ppx-jane" ,ocaml-ppx-jane) |
161 | ("opam" ,opam))) |
162 | (propagated-inputs |
163 | `(("core-kernel" ,ocaml-core-kernel))) |
164 | (build-system ocaml-build-system) |
165 | (arguments janestreet-arguments) |
166 | (home-page "https://github.com/janestreet/core/") |
167 | (synopsis "Alternative to OCaml's standard library") |
168 | (description "The Core suite of libraries is an alternative to OCaml's |
169 | standard library that was developed by Jane Street.") |
170 | (license license:asl2.0))) |
171 | |
172 | (define-public ocaml-async-unix |
173 | (package |
174 | (name "ocaml-async-unix") |
175 | (version "113.33.03") |
176 | (source (janestreet-origin "async_unix" version |
177 | "1fwl0lfrizllcfjk8hk8m7lsz9ha2jg6qgk4gssfyz377qvpcq4h")) |
178 | (native-inputs |
179 | `(("oasis" ,ocaml-oasis) |
180 | ("js-build-tools" ,ocaml-js-build-tools) |
181 | ("ppx-jane" ,ocaml-ppx-jane) |
182 | ("opam" ,opam))) |
183 | (propagated-inputs |
184 | `(("async-kernel" ,ocaml-async-kernel) |
185 | ("core" ,ocaml-core))) |
186 | (build-system ocaml-build-system) |
187 | (arguments janestreet-arguments) |
188 | (home-page "https://github.com/janestreet/async_unix") |
189 | (synopsis "Monadic concurrency library") |
190 | (description "Monadic concurrency library.") |
191 | (license license:asl2.0))) |
192 | |
193 | (define-public ocaml-async-extra |
194 | (package |
195 | (name "ocaml-async-extra") |
196 | (version "113.33.03") |
197 | (source (janestreet-origin "async_extra" version |
198 | "1si8jgiq5xh5sl9f2b7f9p17p7zx5h1pg557x2cxywi2x7pxqg4f")) |
199 | (native-inputs |
200 | `(("oasis" ,ocaml-oasis) |
201 | ("js-build-tools" ,ocaml-js-build-tools) |
202 | ("ppx-jane" ,ocaml-ppx-jane) |
203 | ("opam" ,opam))) |
204 | (propagated-inputs |
205 | `(("async-rpc-kernel" ,ocaml-async-rpc-kernel) |
206 | ("async-unix" ,ocaml-async-unix) |
207 | ("core" ,ocaml-core))) |
208 | (build-system ocaml-build-system) |
209 | (arguments janestreet-arguments) |
210 | (home-page "https://github.com/janestreet/async_extra") |
211 | (synopsis "Monadic concurrency library") |
212 | (description "Monadic concurrency library.") |
213 | (license license:asl2.0))) |
214 | |
215 | (define-public ocaml-async |
216 | (package |
217 | (name "ocaml-async") |
218 | (version "113.33.03") |
219 | (source (janestreet-origin "async" version |
220 | "0210fyhcs12kpmmd26015bgivkfd2wqkyn3c5wd7688d0f872y25")) |
221 | (native-inputs |
222 | `(("oasis" ,ocaml-oasis) |
223 | ("js-build-tools" ,ocaml-js-build-tools) |
224 | ("ppx-jane" ,ocaml-ppx-jane) |
225 | ("opam" ,opam))) |
226 | (propagated-inputs |
227 | `(("async-extra" ,ocaml-async-extra))) |
228 | (build-system ocaml-build-system) |
229 | (arguments janestreet-arguments) |
230 | (home-page "https://github.com/janestreet/async") |
231 | (synopsis "Monadic concurrency library") |
232 | (description "Monadic concurrency library.") |
233 | (license license:asl2.0))) |
234 | |
235 | (define-public ocaml-ocplib-endian |
236 | (package |
237 | (name "ocaml-ocplib-endian") |
238 | (version "1.0") |
239 | (source (origin |
240 | (method url-fetch) |
241 | (uri (string-append "https://github.com/OCamlPro/ocplib-endian/" |
242 | "archive/" version ".tar.gz")) |
243 | (sha256 |
244 | (base32 |
245 | "0hwj09rnzjs0m0kazz5h2mgs6p95j0zlga8cda5srnzqmzhniwkn")) |
246 | (file-name (string-append name "-" version ".tar.gz")))) |
247 | (build-system ocaml-build-system) |
248 | (native-inputs `(("cppo" ,ocaml-cppo))) |
249 | (home-page "https://github.com/OCamlPro/ocplib-endian") |
250 | (synopsis "Optimised functions to read and write int16/32/64 from strings |
251 | and bigarrays") |
252 | (description "Optimised functions to read and write int16/32/64 from strings |
253 | and bigarrays, based on new primitives added in version 4.01. It works on |
254 | strings, bytes and bigstring (Bigarrys of chars), and provides submodules for |
255 | big- and little-endian, with their unsafe counter-parts.") |
256 | (license license:lgpl2.1))) |
257 | |
258 | (define-public ocaml-cstruct |
259 | (package |
260 | (name "ocaml-cstruct") |
261 | (version "2.3.1") |
262 | (source (origin |
263 | (method url-fetch) |
264 | (uri (string-append "https://github.com/mirage/ocaml-cstruct/" |
265 | "archive/v" version ".tar.gz")) |
266 | (sha256 |
267 | (base32 |
268 | "15qpdc8421shq4pprdas9jznpva45229wkfqbwcxw9khaiiz7949")) |
269 | (file-name (string-append name "-" version ".tar.gz")))) |
270 | (build-system ocaml-build-system) |
271 | (arguments |
272 | `(#:configure-flags |
273 | (list "--enable-lwt" "--enable-async") |
274 | #:phases |
275 | (modify-phases %standard-phases |
276 | (add-after 'install 'link-stubs |
277 | (lambda* (#:key outputs #:allow-other-keys) |
278 | (let* ((out (assoc-ref outputs "out")) |
279 | (stubs (string-append out "/lib/ocaml/site-lib/stubslibs")) |
280 | (lib (string-append out "/lib/ocaml/site-lib/cstruct"))) |
281 | (mkdir-p stubs) |
282 | (symlink (string-append lib "/dllcstruct_stubs.so") |
283 | (string-append stubs "/dllcstruct_stubs.so")))))))) |
284 | (native-inputs |
285 | `(("ounit" ,ocaml-ounit) |
286 | ("ppx-tools" ,ocaml-ppx-tools) |
287 | ("camlp4" ,camlp4))) |
288 | (propagated-inputs |
289 | `(("ocplib-endian" ,ocaml-ocplib-endian) |
290 | ("lwt" ,ocaml-lwt) |
291 | ("async" ,ocaml-async) |
292 | ("sexplib" ,ocaml-sexplib))) |
293 | (home-page "https://github.com/mirage/ocaml-cstruct") |
294 | (synopsis "Access C structures via a camlp4 extension") |
295 | (description "Cstruct is a library and syntax extension to make it easier |
296 | to access C-like structures directly from OCaml. It supports both reading and |
297 | writing to these structures, and they are accessed via the Bigarray module.") |
298 | (license license:isc))) |
299 | |
300 | (define-public ocaml-hex |
301 | (package |
302 | (name "ocaml-hex") |
303 | (version "1.0.0") |
304 | (source (origin |
305 | (method url-fetch) |
306 | (uri (string-append "https://github.com/mirage/ocaml-hex/" |
307 | "archive/" version ".tar.gz")) |
308 | (sha256 |
309 | (base32 |
310 | "0s63g0b8gfv2xm6fv6xg7bva8h76b5pcjb0zw3f8cygs0lq9072v")) |
311 | (file-name (string-append name "-" version ".tar.gz")))) |
312 | (build-system ocaml-build-system) |
313 | (propagated-inputs `(("cstruct" ,ocaml-cstruct))) |
314 | (home-page "https://github.com/mirage/ocaml-hex/") |
315 | (synopsis "Minimal library providing hexadecimal converters") |
316 | (description "Minimal library providing hexadecimal converters.") |
317 | (license license:isc))) |
318 | |
319 | (define-public ocaml-ezjsonm |
320 | (package |
321 | (name "ocaml-ezjsonm") |
322 | (version "0.4.3") |
323 | (source (origin |
324 | (method url-fetch) |
325 | (uri (string-append "https://github.com/mirage/ezjsonm/archive/" |
326 | version ".tar.gz")) |
327 | (sha256 |
328 | (base32 |
329 | "1kag0z2xlk4rw73a240dmkxh9rj6psxxcxkm7d7z0rrj6hzjajgq")) |
330 | (file-name (string-append name "-" version ".tar.gz")))) |
331 | (build-system ocaml-build-system) |
332 | (native-inputs |
333 | `(("alcotest" ,ocaml-alcotest))) |
334 | (propagated-inputs |
335 | `(("hex" ,ocaml-hex) |
336 | ("jsonm" ,ocaml-jsonm) |
337 | ("lwt" ,ocaml-lwt) |
338 | ("sexplib" ,ocaml-sexplib))) |
339 | (arguments |
340 | `(#:configure-flags (list "--enable-lwt") |
341 | ;; dllcstruct_stubs.so: cannot open shared object file: No such file |
342 | ;; or directory. May be fixed? |
343 | #:tests? #f)) |
344 | (home-page "https://github.com/mirage/ezjsonm/") |
345 | (synopsis "An easy interface on top of the Jsonm library") |
346 | (description "This version provides more convenient (but far less flexible) |
347 | input and output functions that go to and from [string] values. This avoids |
348 | the need to write signal code, which is useful for quick scripts that |
349 | manipulate JSON.") |
350 | (license license:isc))) |
351 | |
352 | (define-public ocaml-uri |
353 | (package |
354 | (name "ocaml-uri") |
355 | (version "1.9.2") |
356 | (source (origin |
357 | (method url-fetch) |
358 | (uri (string-append "https://github.com/mirage/ocaml-uri/archive/v" |
359 | version ".tar.gz")) |
360 | (sha256 |
361 | (base32 |
362 | "02bzrag79prx261rxf9mlak749pwf4flpfl8p012x1xznv9m0clc")) |
363 | (file-name (string-append name "-" version ".tar.gz")))) |
364 | (build-system ocaml-build-system) |
365 | (native-inputs |
366 | `(("ounit" ,ocaml-ounit))) |
367 | (propagated-inputs |
368 | `(("ppx-sexp-conv" ,ocaml-ppx-sexp-conv) |
369 | ("re" ,ocaml-re) |
370 | ("ppx-deriving" ,ocaml-ppx-deriving) |
371 | ("sexplib" ,ocaml-sexplib) |
372 | ("stringext" ,ocaml-stringext))) |
373 | (home-page "https://github.com/mirage/ocaml-uri") |
374 | (synopsis "RFC3986 URI/URL parsing library") |
375 | (description "RFC3986 URI/URL parsing library.") |
376 | (license license:isc))) |
377 | |
378 | (define-public ocaml-easy-format |
379 | (package |
380 | (name "ocaml-easy-format") |
381 | (version "1.2.0") |
382 | (source (origin |
383 | (method url-fetch) |
384 | (uri (string-append "https://github.com/mjambon/easy-format/" |
385 | "archive/v" version ".tar.gz")) |
386 | (sha256 |
387 | (base32 |
388 | "1zcz682y9figa84k7lgdjcab5qbzk3yy14ygfqp2dhhrvjygm252")) |
389 | (file-name (string-append name "-" version ".tar.gz")))) |
390 | (build-system ocaml-build-system) |
391 | (arguments |
392 | `(#:phases |
393 | (modify-phases %standard-phases |
394 | (delete 'configure)) |
395 | #:tests? #f)) |
396 | (home-page "https://github.com/mjambon/easy-format") |
397 | (synopsis "High-level and functional interface to the Format module of the |
398 | OCaml standard library") |
399 | (description "High-level and functional interface to the Format module of |
400 | the OCaml standard library.") |
401 | (license license:bsd-3))) |
402 | |
403 | (define-public ocaml-optcomp |
404 | (package |
405 | (name "ocaml-optcomp") |
406 | (version "1.6") |
407 | (source (origin |
408 | (method url-fetch) |
409 | (uri (string-append "https://github.com/diml/optcomp/archive/" |
410 | version ".tar.gz")) |
411 | (sha256 |
412 | (base32 |
413 | "0hhhb2gisah1h22zlg5iszbgqxdd7x85cwd57bd4mfkx9l7dh8jh")) |
414 | (file-name (string-append name "-" version ".tar.gz")))) |
415 | (build-system ocaml-build-system) |
416 | (arguments |
417 | `(#:use-make? #t |
418 | #:make-flags |
419 | (list (string-append "BUILDFLAGS=\"-cflags -I," |
420 | (assoc-ref %build-inputs "camlp4") |
421 | "/lib/ocaml/site-lib/camlp4/Camlp4Parsers\"")))) |
422 | (native-inputs `(("camlp4" ,camlp4))) |
423 | (propagated-inputs `(("camlp4" ,camlp4))) |
424 | (home-page "https://github.com/diml/optcomp") |
425 | (synopsis "Optional compilation with cpp-like directives") |
426 | (description "Optional compilation with cpp-like directives.") |
427 | (license license:bsd-3))) |
428 | |
429 | (define-public ocaml-piqilib |
430 | (package |
431 | (name "ocaml-piqilib") |
432 | (version "0.6.13") |
433 | (source (origin |
434 | (method url-fetch) |
435 | (uri (string-append "https://github.com/alavrik/piqi/archive/v" |
436 | version ".tar.gz")) |
437 | (sha256 |
438 | (base32 |
439 | "1whqr2bb3gds2zmrzqnv8vqka9928w4lx6mi6g244kmbwb2h8d8l")) |
440 | (file-name (string-append name "-" version ".tar.gz")) |
441 | (patches (search-patches "ocaml-piqilib-fix-makefile.patch")))) |
442 | (build-system ocaml-build-system) |
443 | (arguments |
444 | `(#:phases |
445 | (modify-phases %standard-phases |
446 | (replace 'configure |
447 | (lambda* (#:key outputs #:allow-other-keys) |
448 | (let ((out (assoc-ref outputs "out"))) |
449 | (substitute* "make/OCamlMakefile" |
450 | (("/bin/sh") (which "bash"))) |
451 | (zero? (system* "./configure" "--prefix" out "--ocaml-libdir" |
452 | (string-append out "/lib/ocaml/site-lib")))))) |
453 | (add-after 'build 'build-ocaml |
454 | (lambda* (#:key outputs #:allow-other-keys) |
455 | (zero? (system* "make" "ocaml")))) |
456 | (add-after 'install 'install-ocaml |
457 | (lambda* (#:key outputs #:allow-other-keys) |
458 | (zero? (system* "make" "ocaml-install")))) |
459 | (add-after 'install-ocaml 'link-stubs |
460 | (lambda* (#:key outputs #:allow-other-keys) |
461 | (let* ((out (assoc-ref outputs "out")) |
462 | (stubs (string-append out "/lib/ocaml/site-lib/stubslibs")) |
463 | (lib (string-append out "/lib/ocaml/site-lib/piqilib"))) |
464 | (mkdir-p stubs) |
465 | (symlink (string-append lib "/dllpiqilib_stubs.so") |
466 | (string-append stubs "/dllpiqilib_stubs.so")))))))) |
467 | (native-inputs |
468 | `(("which" ,which) |
469 | ("camlp4" ,camlp4))) |
470 | (propagated-inputs |
471 | `(("xmlm" ,ocaml-xmlm) |
472 | ("ulex" ,ocaml-ulex) |
473 | ("optcomp" ,ocaml-optcomp) |
474 | ("easy-format" ,ocaml-easy-format) |
475 | ("base64" ,ocaml-base64))) |
476 | (home-page "http://piqi.org") |
477 | (synopsis "Data serialization and conversion library") |
478 | (description "Common library used by piqi command-line tool and piqi-ocaml.") |
479 | (license license:asl2.0))) |
480 | |
481 | (define-public ocaml-uuidm |
482 | (package |
483 | (name "ocaml-uuidm") |
484 | (version "0.9.6") |
485 | (source (origin |
486 | (method url-fetch) |
487 | (uri (string-append "http://erratique.ch/software/uuidm/" |
488 | "releases/uuidm-" version ".tbz")) |
489 | (sha256 |
490 | (base32 |
491 | "0hz4fdx0x16k0pw9995vkz5d1hmzz6b16wck9li399rcbfnv5jlc")))) |
492 | (build-system ocaml-build-system) |
493 | (arguments |
494 | `(#:tests? #f |
495 | #:build-flags |
496 | (list "build" "--with-cmdliner" "true") |
497 | #:phases |
498 | (modify-phases %standard-phases |
499 | (delete 'configure)))) |
500 | (native-inputs |
501 | `(("opam" ,opam))) |
502 | (propagated-inputs |
503 | `(("cmdliner" ,ocaml-cmdliner) |
504 | ("topkg" ,ocaml-topkg))) |
505 | (home-page "http://erratique.ch/software/uuidm") |
506 | (synopsis "Universally unique identifiers (UUIDs) for OCaml") |
507 | (description "Uuidm is an OCaml module implementing 128 bits universally |
508 | unique identifiers version 3, 5 (named based with MD5, SHA-1 hashing) and 4 |
509 | (random based) according to RFC 4122.") |
510 | (license license:isc))) |
511 | |
512 | (define-public ocamlgraph |
513 | (package |
514 | (name "ocamlgraph") |
515 | (version "1.8.7") |
516 | (source (origin |
517 | (method url-fetch) |
518 | (uri (string-append "http://ocamlgraph.lri.fr/download/" |
519 | "ocamlgraph-" version ".tar.gz")) |
520 | (sha256 |
521 | (base32 |
522 | "1845r537swjil2fcj7lgbibc2zybfwqqasrd2s7bncajs83cl1nz")) |
523 | (patches (search-patches "ocamlgraph-honor-source-date-epoch.patch")))) |
524 | (build-system ocaml-build-system) |
525 | (arguments |
526 | `(#:install-target "install-findlib" |
527 | #:phases |
528 | (modify-phases %standard-phases |
529 | (add-before 'configure 'fix-/bin/sh |
530 | (lambda* (#:key inputs #:allow-other-keys) |
531 | (substitute* "configure" |
532 | (("-/bin/sh") (string-append "-" (assoc-ref inputs "bash") |
533 | "/bin/sh")))))))) |
534 | (inputs `(("lablgtk" ,lablgtk))) |
535 | (home-page "http://ocamlgraph.lri.fr/") |
536 | (synopsis "A generic graph library for OCaml") |
537 | (description "A generic graph library for OCaml.") |
538 | (license license:lgpl2.1))) |
539 | |
540 | (define-public ocaml-piqi |
541 | (package |
542 | (name "ocaml-piqi") |
543 | (version "0.7.5") |
544 | (source (origin |
545 | (method url-fetch) |
546 | (uri (string-append "https://github.com/alavrik/piqi-ocaml/" |
547 | "archive/v" version ".tar.gz")) |
548 | (sha256 |
549 | (base32 |
550 | "0ngz6y8i98i5v2ma8nk6mc83pdsmf2z0ks7m3xi6clfg3zqbddrv")))) |
551 | (build-system ocaml-build-system) |
552 | (arguments |
553 | `(#:make-flags |
554 | (list (string-append "DESTDIR=" (assoc-ref %outputs "out"))) |
555 | #:phases |
556 | (modify-phases %standard-phases |
557 | (delete 'configure) |
558 | (add-before 'build 'patch-/bin/sh |
559 | (lambda _ |
560 | (substitute* "make/OCamlMakefile" |
561 | (("/bin/sh") (which "sh"))) |
562 | #t))))) |
563 | (native-inputs |
564 | `(("which" ,which) |
565 | ("protobuf" ,protobuf))) ; for tests |
566 | (propagated-inputs |
567 | `(("piqilib" ,ocaml-piqilib))) |
568 | (home-page "https://github.com/alavrik/piqi-ocaml") |
569 | (synopsis "Protocol serialization system for OCaml") |
570 | (description "Piqi is a multi-format data serialization system for OCaml. |
571 | It provides a uniform interface for serializing OCaml data structures to JSON, |
572 | XML and Protocol Buffers formats.") |
573 | (license license:asl2.0))) |
574 | |
575 | (define-public bap |
576 | (package |
577 | (name "bap") |
578 | (version "1.1.0") |
579 | (home-page "https://github.com/BinaryAnalysisPlatform/bap") |
580 | (source (origin |
581 | (method url-fetch) |
582 | (uri (string-append home-page "/archive/v" version ".tar.gz")) |
583 | (sha256 |
584 | (base32 |
585 | "1ms95m4j1qrmy7zqmsn2izh7gq68lnmssl7chyhk977kd3sxj66m")) |
586 | (file-name (string-append name "-" version ".tar.gz")))) |
587 | (build-system ocaml-build-system) |
588 | (native-inputs |
589 | `(("oasis" ,ocaml-oasis) |
590 | ("clang" ,clang) |
591 | ("ounit" ,ocaml-ounit))) |
592 | (propagated-inputs |
593 | `(("core-kernel" ,ocaml-core-kernel) |
594 | ("ppx-driver" ,ocaml-ppx-driver) |
595 | ("uri" ,ocaml-uri) |
596 | ("llvm" ,llvm) |
597 | ("gmp" ,gmp) |
598 | ("clang-runtime" ,clang-runtime) |
599 | ("fileutils" ,ocaml-fileutils) |
600 | ("cmdliner" ,ocaml-cmdliner) |
601 | ("zarith" ,ocaml-zarith) |
602 | ("uuidm" ,ocaml-uuidm) |
603 | ("camlzip" ,camlzip) |
604 | ("frontc" ,ocaml-frontc) |
605 | ("ezjsonm" ,ocaml-ezjsonm) |
606 | ("ocurl" ,ocaml-ocurl) |
607 | ("piqi" ,ocaml-piqi) |
608 | ("ocamlgraph" ,ocamlgraph) |
609 | ("bitstring" ,ocaml-bitstring) |
610 | ("ppx-jane" ,ocaml-ppx-jane) |
611 | ("re" ,ocaml-re))) |
612 | (inputs `(("llvm" ,llvm))) |
613 | (arguments |
614 | `(#:use-make? #t |
615 | #:phases |
616 | (modify-phases %standard-phases |
617 | (replace 'configure |
618 | (lambda* (#:key outputs #:allow-other-keys) |
619 | (zero? (system* "./configure" "--prefix" |
620 | (assoc-ref outputs "out") |
621 | "--libdir" |
622 | (string-append |
623 | (assoc-ref outputs "out") |
624 | "/lib/ocaml/site-lib") |
625 | "--with-llvm-version=3.8" |
626 | "--with-llvm-config=llvm-config" |
627 | "--enable-everything")))) |
628 | (add-before 'install 'fix-ocamlpath |
629 | (lambda* (#:key outputs #:allow-other-keys) |
630 | (setenv "OCAMLPATH" |
631 | (string-append |
632 | (getenv "OCAMLPATH") ":" |
633 | (assoc-ref outputs "out") |
634 | "/lib/ocaml/site-lib")) |
635 | (setenv "PATH" |
636 | (string-append (getenv "PATH") ":" |
637 | (assoc-ref outputs "out") "/bin")))) |
638 | (add-after 'install 'link-stubs |
639 | (lambda* (#:key outputs #:allow-other-keys) |
640 | (let* ((out (assoc-ref outputs "out")) |
641 | (stubs (string-append out "/lib/ocaml/site-lib/stubslibs")) |
642 | (lib (string-append out "/lib/ocaml/site-lib/bap-plugin-llvm"))) |
643 | (mkdir-p stubs) |
644 | (symlink (string-append lib "/dllllvm_plugin_stubs.so") |
645 | (string-append stubs "/dllllvm_plugin_stubs.so")))))))) |
646 | (synopsis "Binary Analysis Platform") |
647 | (description "Binary Analysis Platform is a framework for writing program |
648 | analysis tools, that target binary files. The framework consists of a plethora |
649 | of libraries, plugins, and frontends. The libraries provide code reusability, |
650 | the plugins facilitate extensibility, and the frontends serve as entry points.") |
651 | (license license:expat))) |
652 | |
653 | (define-public ocaml-camomile |
654 | (package |
655 | (name "ocaml-camomile") |
656 | (version "0.8.5") |
657 | (home-page "https://github.com/yoriyuki/Camomile") |
658 | (source (origin |
659 | (method url-fetch) |
660 | (uri (string-append home-page "/releases/download/rel-" version |
661 | "/camomile-" version ".tar.bz2")) |
662 | (sha256 |
663 | (base32 |
664 | "003ikpvpaliy5hblhckfmln34zqz0mk3y2m1fqvbjngh3h2np045")))) |
665 | (build-system ocaml-build-system) |
666 | (native-inputs `(("camlp4" ,camlp4))) |
667 | (arguments |
668 | `(#:phases |
669 | (modify-phases %standard-phases |
670 | (add-before 'configure 'fix-bin/sh |
671 | (lambda* (#:key #:allow-other-keys) |
672 | (substitute* "configure" |
673 | (("CONFIG_SHELL-/bin/sh") |
674 | (string-append "CONFIG_SHELL-" (which "bash"))))))))) |
675 | (synopsis "Comprehensive Unicode library") |
676 | (description "Camomile is a Unicode library for OCaml. Camomile provides |
677 | Unicode character type, UTF-8, UTF-16, UTF-32 strings, conversion to/from about |
678 | 200 encodings, collation and locale-sensitive case mappings, and more. The |
679 | library is currently designed for Unicode Standard 3.2.") |
680 | (license license:lgpl2.0+))) ; with an exception |
681 | |
682 | (define-public ocaml-zed |
683 | (package |
684 | (name "ocaml-zed") |
685 | (version "1.4") |
686 | (source (origin |
687 | (method url-fetch) |
688 | (uri (string-append "https://github.com/diml/zed/archive/" |
689 | version ".tar.gz")) |
690 | (sha256 |
691 | (base32 |
692 | "0pvfq9ikhbkv4ksn3k3vzs6wiwkihjav3n81lhxm54z9931gfwnz")))) |
693 | (build-system ocaml-build-system) |
694 | (propagated-inputs |
695 | `(("camomile" ,ocaml-camomile) |
696 | ("react" ,ocaml-react))) |
697 | (home-page "https://github.com/diml/zed") |
698 | (synopsis "Abstract engine for text edition in OCaml") |
699 | (description "Zed is an abstract engine for text edition. It can be used to |
700 | write text editors, edition widgets, readlines, ... |
701 | |
702 | Zed uses Camomile to fully support the Unicode specification, and implements an |
703 | UTF-8 encoded string type with validation, and a rope datastructure to achieve |
704 | efficient operations on large Unicode buffers. Zed also features a regular |
705 | expression search on ropes. |
706 | |
707 | To support efficient text edition capabilities, Zed provides macro recording |
708 | and cursor management facilities.") |
709 | (license license:bsd-3))) |
710 | |
711 | (define-public ocaml-lambda-term |
712 | (package |
713 | (name "ocaml-lambda-term") |
714 | (version "1.10.1") |
715 | (home-page "https://github.com/diml/lambda-term") |
716 | (source (origin |
717 | (method url-fetch) |
718 | (uri (string-append home-page "/archive/" version ".tar.gz")) |
719 | (sha256 |
720 | (base32 |
721 | "1449glcsavcwbcsxbd7wcjz50y8vvin4zwpmkhq8i6jca3f3sknj")))) |
722 | (build-system ocaml-build-system) |
723 | (propagated-inputs |
724 | `(("zed" ,ocaml-zed) |
725 | ("lwt" ,ocaml-lwt) |
726 | ("react" ,ocaml-react))) |
727 | (arguments |
728 | `(#:phases |
729 | (modify-phases %standard-phases |
730 | (add-after 'install 'link-stubs |
731 | (lambda* (#:key outputs #:allow-other-keys) |
732 | (let* ((out (assoc-ref outputs "out")) |
733 | (stubs (string-append out "/lib/ocaml/site-lib/stubslibs")) |
734 | (lib (string-append out "/lib/ocaml/site-lib/lambda-term"))) |
735 | (mkdir-p stubs) |
736 | (symlink (string-append lib "/dlllambda-term_stubs.so") |
737 | (string-append stubs "/dlllambda-term_stubs.so")))))))) |
738 | (synopsis "Terminal manipulation library for OCaml") |
739 | (description "Lambda-term is a cross-platform library for manipulating the |
740 | terminal. It provides an abstraction for keys, mouse events, colors, as well as |
741 | a set of widgets to write curses-like applications. |
742 | |
743 | The main objective of lambda-term is to provide a higher level functional |
744 | interface to terminal manipulation than, for example, ncurses, by providing a |
745 | native OCaml interface instead of bindings to a C library. |
746 | |
747 | Lambda-term integrates with zed to provide text edition facilities in console |
748 | applications.") |
749 | (license license:bsd-3))) |
750 | |
751 | (define-public ocaml-utop |
752 | (package |
753 | (name "ocaml-utop") |
754 | (version "1.19.3") |
755 | (source (origin |
756 | (method url-fetch) |
757 | (uri (string-append "https://github.com/diml/utop/archive/" |
758 | version ".tar.gz")) |
759 | (file-name (string-append name "-" version ".tar.gz")) |
760 | (sha256 |
761 | (base32 |
762 | "16z02vp9n97iax4fqpbi7v86r75vbabxvnd1rirh8w2miixs1g4x")))) |
763 | (build-system ocaml-build-system) |
764 | (native-inputs |
765 | `(("cppo" ,ocaml-cppo))) |
766 | (propagated-inputs |
767 | `(("lambda-term" ,ocaml-lambda-term) |
768 | ("lwt" ,ocaml-lwt) |
769 | ("react" ,ocaml-react))) |
770 | (home-page "https://github.com/diml/utop") |
771 | (synopsis "Universal toplevel for OCaml") |
772 | (description "utop is an improved toplevel for OCaml. It can run in a |
773 | terminal or in Emacs. It supports line edition, history, real-time and context |
774 | sensitive completion, colors, and more. |
775 | |
776 | It integrates with the tuareg mode in Emacs.") |
777 | (license license:bsd-3))) |
778 | |
779 | (define-public proof-general2 |
780 | (package |
781 | (name "proof-general2") |
782 | (version "4.4") |
783 | (source (origin |
784 | (method url-fetch) |
785 | (uri (string-append |
786 | "https://github.com/ProofGeneral/PG/archive/v" |
787 | version ".tar.gz")) |
788 | (file-name (string-append name "-" version ".tar.gz")) |
789 | (sha256 |
790 | (base32 |
791 | "0zif2fv6mm4pv75nh10q3p37n293495rvx470bx7ma382zc3d8hv")))) |
792 | (build-system gnu-build-system) |
793 | (native-inputs |
794 | `(("which" ,which) |
795 | ("emacs" ,emacs-minimal) |
796 | ("texinfo" ,texinfo))) |
797 | (inputs |
798 | `(("host-emacs" ,emacs) |
799 | ("perl" ,perl) |
800 | ("coq" ,coq))) |
801 | (arguments |
802 | `(#:tests? #f ; no check target |
803 | #:make-flags (list (string-append "PREFIX=" %output) |
804 | (string-append "DEST_PREFIX=" %output) |
805 | "-j1") |
806 | #:modules ((guix build gnu-build-system) |
807 | (guix build utils) |
808 | (guix build emacs-utils)) |
809 | #:imported-modules (,@%gnu-build-system-modules |
810 | (guix build emacs-utils)) |
811 | #:phases |
812 | (modify-phases %standard-phases |
813 | (delete 'configure) |
814 | (add-after 'unpack 'disable-byte-compile-error-on-warn |
815 | (lambda _ |
816 | (substitute* "Makefile" |
817 | (("\\(setq byte-compile-error-on-warn t\\)") |
818 | "(setq byte-compile-error-on-warn nil)")) |
819 | #t)) |
820 | (add-after 'unpack 'patch-hardcoded-paths |
821 | (lambda* (#:key inputs outputs #:allow-other-keys) |
822 | (let ((out (assoc-ref outputs "out")) |
823 | (coq (assoc-ref inputs "coq")) |
824 | (emacs (assoc-ref inputs "host-emacs"))) |
825 | (define (coq-prog name) |
826 | (string-append coq "/bin/" name)) |
827 | (substitute* "pgshell/pgshell.el" |
828 | (("/bin/sh") (which "sh"))) |
829 | ;(emacs-substitute-variables "coq/coq.el" |
830 | ; ("coq-prog-name" (coq-prog "coqtop")) |
831 | ; ("coq-compiler" (coq-prog "coqc")) |
832 | ; ("coq-dependency-analyzer" (coq-prog "coqdep"))) |
833 | (substitute* "Makefile" |
834 | (("/sbin/install-info") "install-info")) |
835 | (substitute* "bin/proofgeneral" |
836 | (("^PGHOMEDEFAULT=.*" all) |
837 | (string-append all |
838 | "PGHOME=$PGHOMEDEFAULT\n" |
839 | "EMACS=" emacs "/bin/emacs"))) |
840 | #t)))))) |
841 | ;(add-after 'unpack 'clean |
842 | ; (lambda _ |
843 | ; ;; Delete the pre-compiled elc files for Emacs 23. |
844 | ; (zero? (system* "make" "clean")))) |
845 | ;(add-after 'install 'install-doc |
846 | ; (lambda* (#:key make-flags #:allow-other-keys) |
847 | ; ;; XXX FIXME avoid building/installing pdf files, |
848 | ; ;; due to unresolved errors building them. |
849 | ; (substitute* "Makefile" |
850 | ; ((" [^ ]*\\.pdf") "")) |
851 | ; (zero? (apply system* "make" "install-doc" |
852 | ; make-flags))))))) |
853 | (home-page "http://proofgeneral.inf.ed.ac.uk/") |
854 | (synopsis "Generic front-end for proof assistants based on Emacs") |
855 | (description |
856 | "Proof General is a major mode to turn Emacs into an interactive proof |
857 | assistant to write formal mathematical proofs using a variety of theorem |
858 | provers.") |
859 | (license license:gpl2+))) |
860 | |
861 | (define-public compcert |
862 | (package |
863 | (name "compcert") |
864 | (version "3.0") |
865 | (source (origin |
866 | (method url-fetch) |
867 | (uri (string-append "http://compcert.inria.fr/release/compcert-" |
868 | version ".tgz")) |
869 | (sha256 |
870 | (base32 |
871 | "03fxf01acvy0akzb1czk33jsfmv2rka0m0jc1a2gmzs9i192rr7m")))) |
872 | (build-system gnu-build-system) |
873 | (arguments |
874 | `(#:phases |
875 | (modify-phases %standard-phases |
876 | (replace 'configure |
877 | (lambda* (#:key outputs #:allow-other-keys) |
878 | (zero? (system* "./configure" "x86_64-linux" "-prefix" |
879 | (assoc-ref outputs "out")))))) |
880 | #:tests? #f)) |
881 | (native-inputs |
882 | `(("ocaml" ,ocaml) |
883 | ("coq" ,coq))) |
884 | (inputs |
885 | `(("menhir" ,ocaml-menhir))) |
886 | (home-page "http://compcert.inria.fr") |
887 | (synopsis "Certified C compiler") |
888 | (description "CompCert is a certified (with coq) C compiler. Warning: this |
889 | package is not free software!") |
890 | ;; actually the "INRIA Non-Commercial License Agreement" |
891 | ;; a non-free license. |
892 | (license (license:non-copyleft "file:///LICENSE")))) |
893 | |
894 | ;; yet another build system <3 |
895 | ;; In this one, the autoconf-generated configure script configures the build and |
896 | ;; builds remake from source, a make-like system specific to this package. |
897 | (define-public coq-flocq |
898 | (package |
899 | (name "coq-flocq") |
900 | (version "2.5.2") |
901 | (source (origin |
902 | (method url-fetch) |
903 | (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36199/flocq-" |
904 | version ".tar.gz")) |
905 | (sha256 |
906 | (base32 |
907 | "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h")))) |
908 | (build-system gnu-build-system) |
909 | (native-inputs |
910 | `(("ocaml" ,ocaml) |
911 | ("which" ,which) |
912 | ("coq" ,coq))) |
913 | (arguments |
914 | `(#:configure-flags |
915 | (list (string-append "--libdir=" (assoc-ref %outputs "out") |
916 | "/lib/coq/user-contrib/Flocq")) |
917 | #:phases |
918 | (modify-phases %standard-phases |
919 | (add-before 'configure 'fix-remake |
920 | (lambda _ |
921 | (substitute* "remake.cpp" |
922 | (("/bin/sh") (which "sh"))))) |
923 | (replace 'build |
924 | (lambda _ |
925 | (zero? (system* "./remake")))) |
926 | (replace 'check |
927 | (lambda _ |
928 | (zero? (system* "./remake" "check")))) |
929 | ;; TODO: requires coq-gappa and coq-interval. |
930 | ;(zero? (system* "./remake" "check-more")))) |
931 | (replace 'install |
932 | (lambda _ |
933 | (zero? (system* "./remake" "install"))))))) |
934 | (home-page "http://flocq.gforge.inria.fr/") |
935 | (synopsis "Floating-point formalization for the Coq system") |
936 | (description "Flocq (Floats for Coq) is a floating-point formalization for |
937 | the Coq system. It provides a comprehensive library of theorems on a multi-radix |
938 | multi-precision arithmetic. It also supports efficient numerical computations |
939 | inside Coq.") |
940 | (license license:lgpl3+))) |
941 | |
942 | (define-public coq-gappa |
943 | (package |
944 | (name "coq-gappa") |
945 | (version "1.3.1") |
946 | (source (origin |
947 | (method url-fetch) |
948 | (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36351/gappa-" |
949 | version ".tar.gz")) |
950 | (sha256 |
951 | (base32 |
952 | "0924jr6f15fx22qfsvim5vc0qxqg30ivg9zxj34lf6slbgdl3j39")))) |
953 | (build-system gnu-build-system) |
954 | (native-inputs |
955 | `(("ocaml" ,ocaml) |
956 | ("which" ,which) |
957 | ("coq" ,coq) |
958 | ("bison" ,bison) |
959 | ("flex" ,flex))) |
960 | (inputs |
961 | `(("gmp" ,gmp) |
962 | ("mpfr" ,mpfr) |
963 | ("boost" ,boost))) |
964 | (arguments |
965 | `(#:configure-flags |
966 | (list (string-append "--libdir=" (assoc-ref %outputs "out") |
967 | "/lib/coq/user-contrib/Gappa")) |
968 | #:phases |
969 | (modify-phases %standard-phases |
970 | (add-before 'configure 'fix-remake |
971 | (lambda _ |
972 | (substitute* "remake.cpp" |
973 | (("/bin/sh") (which "sh"))))) |
974 | (replace 'build |
975 | (lambda _ |
976 | (zero? (system* "./remake")))) |
977 | (replace 'check |
978 | (lambda _ |
979 | (zero? (system* "./remake" "check")))) |
980 | (replace 'install |
981 | (lambda _ |
982 | (zero? (system* "./remake" "install"))))))) |
983 | (home-page "http://gappa.gforge.inria.fr/") |
984 | (synopsis "Verify and formally prove properties on numerical programs") |
985 | (description "Gappa is a tool intended to help verifying and formally proving |
986 | properties on numerical programs dealing with floating-point or fixed-point |
987 | arithmetic. It has been used to write robust floating-point filters for CGAL |
988 | and it is used to certify elementary functions in CRlibm. While Gappa is |
989 | intended to be used directly, it can also act as a backend prover for the Why3 |
990 | software verification plateform or as an automatic tactic for the Coq proof |
991 | assistant.") |
992 | (license (list license:gpl2 license:cecill)))) |
993 | |
994 | (define-public coq-mathcomp |
995 | (package |
996 | (name "coq-mathcomp") |
997 | (version "1.6.1") |
998 | (source (origin |
999 | (method url-fetch) |
1000 | (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-" |
1001 | version ".tar.gz")) |
1002 | (sha256 |
1003 | (base32 |
1004 | "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw")))) |
1005 | (build-system gnu-build-system) |
1006 | (native-inputs |
1007 | `(("ocaml" ,ocaml) |
1008 | ("which" ,which) |
1009 | ("coq" ,coq))) |
1010 | (arguments |
1011 | `(#:tests? #f; No need to test formally-verified programs :) |
1012 | #:phases |
1013 | (modify-phases %standard-phases |
1014 | (delete 'configure) |
1015 | (add-before 'build 'chdir |
1016 | (lambda _ |
1017 | (chdir "mathcomp"))) |
1018 | (replace 'install |
1019 | (lambda* (#:key outputs #:allow-other-keys) |
1020 | (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) |
1021 | (zero? (system* "make" "-f" "Makefile.coq" |
1022 | (string-append "COQLIB=" (assoc-ref outputs "out") |
1023 | "/lib/coq/") |
1024 | "install"))))))) |
1025 | (home-page "https://math-comp.github.io/math-comp/") |
1026 | (synopsis "Mathematical Components for Coq") |
1027 | (description "Mathematical Components for Coq has its origins in the formal |
1028 | proof of the Four Colour Theorem. Since then it has grown to cover many areas |
1029 | of mathematics and has been used for large scale projects like the formal proof |
1030 | of the Odd Order Theorem. |
1031 | |
1032 | The library is written using the Ssreflect proof language that is an integral |
1033 | part of the distribution.") |
1034 | (license license:cecill-b))) |
1035 | |
1036 | ;; TODO: coquelicot |
1037 | |
1038 | (define-public coq-interval |
1039 | (package |
1040 | (name "coq-interval") |
1041 | (version "3.2.0") |
1042 | (source (origin |
1043 | (method url-fetch) |
1044 | (uri (string-append "https://gforge.inria.fr/frs/download.php/" |
1045 | "file/36538/interval-" version ".tar.gz")) |
1046 | (sha256 |
1047 | (base32 |
1048 | "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3")))) |
1049 | (build-system gnu-build-system) |
1050 | (native-inputs |
1051 | `(("ocaml" ,ocaml) |
1052 | ("which" ,which) |
1053 | ("coq" ,coq))) |
1054 | (propagated-inputs |
1055 | `(("flocq" ,coq-flocq) |
1056 | ("mathcomp" ,coq-mathcomp))) |
1057 | (arguments |
1058 | `(#:configure-flags |
1059 | (list (string-append "--libdir=" (assoc-ref %outputs "out") |
1060 | "/lib/coq/user-contrib/Gappa")) |
1061 | #:phases |
1062 | (modify-phases %standard-phases |
1063 | (add-before 'configure 'fix-remake |
1064 | (lambda _ |
1065 | (substitute* "remake.cpp" |
1066 | (("/bin/sh") (which "sh"))))) |
1067 | (replace 'build |
1068 | (lambda _ |
1069 | (zero? (system* "./remake")))) |
1070 | (replace 'check |
1071 | (lambda _ |
1072 | (zero? (system* "./remake" "check")))) |
1073 | (replace 'install |
1074 | (lambda _ |
1075 | (zero? (system* "./remake" "install"))))))) |
1076 | (home-page "http://coq-interval.gforge.inria.fr/") |
1077 | (synopsis "Coq tactics to simplify inequality proofs") |
1078 | (description "Interval provides vernacular files containing tactics for |
1079 | simplifying the proofs of inequalities on expressions of real numbers for the |
1080 | Coq proof assistant.") |
1081 | (license license:cecill-c))) |
1082 |