guix-more/more/packages/ocaml.scm

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