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-qcheck
80
  (package
81
    (name "ocaml-qcheck")
82
    (version "0.5.3.1")
83
    (source (origin
84
              (method url-fetch)
85
              (uri (string-append "https://github.com/c-cube/qcheck/archive/"
86
                                  version ".tar.gz"))
87
              (file-name (string-append name "-" version ".tar.gz"))
88
              (sha256
89
               (base32
90
                "1zs1pg5cb1iry554v3cdmmiglsrwmsqa9x8zxmzb118fnk5d3ha6"))))
91
    (build-system ocaml-build-system)
92
    (native-inputs
93
     `(("ounit" ,ocaml-ounit)))
94
    (home-page "https://github.com/c-cube/qcheck")
95
    (synopsis "QuickCheck inspired property-based testing for OCaml")
96
    (description "QuickCheck inspired property-based testing for OCaml. This
97
module allows to check invariants (properties of some types) over randomly
98
generated instances of the type. It provides combinators for generating
99
instances and printing them.")
100
    (license license:lgpl3+)))
101
102
(define-public ocaml-ppx-sexp-value
103
  (package
104
    (name "ocaml-ppx-sexp-value")
105
    (version "113.33.03")
106
    (source (janestreet-origin "ppx_sexp_value" version
107
              "0m3ag23mbqm0i2pv1dzilfks15ipa5q60mf57a0cd3p0pvarq10g"))
108
    (build-system ocaml-build-system)
109
    (native-inputs
110
     `(("js-build-tools" ,ocaml-js-build-tools)
111
       ("opam" ,opam)))
112
    (propagated-inputs
113
     `(("ppx-driver" ,ocaml-ppx-driver)
114
       ("ppx-here" ,ocaml-ppx-here)
115
       ("ppx-sexp-conv" ,ocaml-ppx-sexp-conv)
116
       ("ppx-tools" ,ocaml-ppx-tools)
117
       ("ppx-core" ,ocaml-ppx-core)))
118
    (arguments janestreet-arguments)
119
    (home-page "https://github.com/janestreet/ppx_sexp_value/")
120
    (synopsis "Simplify building s-expressions from ocaml values")
121
    (description "A ppx rewriter that simplifies building s-expressions from
122
ocaml values.")
123
    (license license:asl2.0)))
124
125
(define-public ocaml-ppx-pipebang
126
  (package
127
    (name "ocaml-ppx-pipebang")
128
    (version "113.33.03")
129
    (source (janestreet-origin "ppx_pipebang" version
130
              "1965c7hymp26ncmjs0pfxi2s5jlj60z2c9b194lgcwxqiav56pcw"))
131
    (build-system ocaml-build-system)
132
    (native-inputs
133
     `(("js-build-tools" ,ocaml-js-build-tools)
134
       ("opam" ,opam)))
135
    (propagated-inputs
136
     `(("ppx-driver" ,ocaml-ppx-driver)
137
       ("ppx-tools" ,ocaml-ppx-tools)
138
       ("ppx-core" ,ocaml-ppx-core)))
139
    (arguments janestreet-arguments)
140
    (home-page "https://github.com/janestreet/ppx_pipebang/")
141
    (synopsis "Inline reverse application operators `|>` and `|!`")
142
    (description "A ppx rewriter that inlines reverse application operators
143
`|>` and `|!`.")
144
    (license license:asl2.0)))
145
146
(define-public ocaml-ppx-bin-prot
147
  (package
148
    (name "ocaml-ppx-bin-prot")
149
    (version "113.33.03")
150
    (source (janestreet-origin "ppx_bin_prot" version
151
              "173kjv36giik11zgfvsbzwfbpr66dm2pcha9vf990jgzh8hqz39h"))
152
    (build-system ocaml-build-system)
153
    (native-inputs
154
     `(("js-build-tools" ,ocaml-js-build-tools)
155
       ("opam" ,opam)))
156
    (propagated-inputs
157
     `(("bin-prot" ,ocaml-bin-prot)
158
       ("ppx-tools" ,ocaml-ppx-tools)
159
       ("ppx-type-conv" ,ocaml-ppx-type-conv)
160
       ("ppx-core" ,ocaml-ppx-core)))
161
    (arguments janestreet-arguments)
162
    (home-page "https://github.com/janestreet/ppx_bin_prot/")
163
    (synopsis "Generation of bin_prot readers and writers from types")
164
    (description "Generation of binary serialization and deserialization
165
functions from type definitions.")
166
    (license license:asl2.0)))
167
168
(define-public ocaml-ppx-fail
169
  (package
170
    (name "ocaml-ppx-fail")
171
    (version "113.33.03")
172
    (source (janestreet-origin "ppx_fail" version
173
              "1dwgad0f05gqp5rnwf9dcasidpfi7q3mrpazsw3a2vijjblbhjgn"))
174
    (build-system ocaml-build-system)
175
    (native-inputs
176
     `(("js-build-tools" ,ocaml-js-build-tools)
177
       ("opam" ,opam)))
178
    (propagated-inputs
179
     `(("ppx-driver" ,ocaml-ppx-driver)
180
       ("ppx-tools" ,ocaml-ppx-tools)
181
       ("ppx-here" ,ocaml-ppx-here)
182
       ("ppx-core" ,ocaml-ppx-core)))
183
    (arguments janestreet-arguments)
184
    (home-page "https://github.com/janestreet/ppx_fail/")
185
    (synopsis "Add location to calls to failwiths")
186
    (description "Syntax extension that makes [failwiths] always include a
187
position.")
188
    (license license:asl2.0)))
189
190
(define-public ocaml-ppx-custom-printf
191
  (package
192
    (name "ocaml-ppx-custom-printf")
193
    (version "113.33.03")
194
    (source (janestreet-origin "ppx_custom_printf" version
195
              "11jlx0n87g2j1vyyp343dibx7lvvwig5j5q0nq0b80kbsq0k6yr8"))
196
    (build-system ocaml-build-system)
197
    (native-inputs
198
     `(("js-build-tools" ,ocaml-js-build-tools)
199
       ("opam" ,opam)))
200
    (propagated-inputs
201
     `(("ppx-sexp-conv" ,ocaml-ppx-sexp-conv)
202
       ("ppx-tools" ,ocaml-ppx-tools)
203
       ("ppx-core" ,ocaml-ppx-core)
204
       ("ppx-driver" ,ocaml-ppx-driver)))
205
    (arguments janestreet-arguments)
206
    (home-page "https://github.com/janestreet/ppx_custom_printf/")
207
    (synopsis "Printf-style format-strings for user-defined string conversion")
208
    (description "Extensions to printf-style format-strings for user-defined
209
string conversion.")
210
    (license license:asl2.0)))
211
212
(define-public ocaml-ppx-sexp-message
213
  (package
214
    (name "ocaml-ppx-sexp-message")
215
    (version "113.33.03")
216
    (source (janestreet-origin "ppx_sexp_message" version
217
              "084w1l3gnyw4ri9vbn7bv9b2xkw1520qczfxpxdarfivdrz8xr68"))
218
    (build-system ocaml-build-system)
219
    (native-inputs
220
     `(("js-build-tools" ,ocaml-js-build-tools)
221
       ("opam" ,opam)))
222
    (propagated-inputs
223
     `(("ppx-driver" ,ocaml-ppx-driver)
224
       ("ppx-here" ,ocaml-ppx-here)
225
       ("ppx-sexp-conv" ,ocaml-ppx-sexp-conv)
226
       ("ppx-tools" ,ocaml-ppx-tools)
227
       ("ppx-core" ,ocaml-ppx-core)))
228
    (arguments janestreet-arguments)
229
    (home-page "https://github.com/janestreet/ppx_sexp_message/")
230
    (synopsis "A ppx rewriter for easy construction of s-expressions")
231
    (description "The aim of ppx_sexp_message is to ease the creation of
232
s-expressions in OCaml.  This is mainly motivated by writing error and debugging
233
messages, where one needs to construct a s-expression based on various element
234
of the context such as function arguments.")
235
    (license license:asl2.0)))
236
237
(define-public ocaml-ppx-fields-conv
238
  (package
239
    (name "ocaml-ppx-fields-conv")
240
    (version "113.33.03")
241
    (source (janestreet-origin "ppx_fields_conv" version
242
              "1vzbdz27g5qhhfs7wx6rjf979q4xyssxqbmp6sc1sxknbghslbdv"))
243
    (build-system ocaml-build-system)
244
    (native-inputs
245
     `(("js-build-tools" ,ocaml-js-build-tools)
246
       ("opam" ,opam)
247
       ("ppx-core" ,ocaml-ppx-core)))
248
    (propagated-inputs
249
     `(("fieldslib" ,ocaml-fieldslib)
250
       ("ppx-tools" ,ocaml-ppx-tools)
251
       ("ppx-core" ,ocaml-ppx-core)
252
       ("ppx-type-conv" ,ocaml-ppx-type-conv)))
253
    (arguments janestreet-arguments)
254
    (home-page "https://github.com/janestreet/ppx_fields_conv/")
255
    (synopsis "Generation of accessor and iteration functions for ocaml records")
256
    (description "Ppx_fields_conv is a ppx rewriter that can be used to define
257
first class values representing record fields, and additional routines, to get
258
and set record fields, iterate and fold over all fields of a record and create
259
new record values.")
260
    (license license:asl2.0)))
261
262
(define-public ocaml-re
263
  (package
264
    (name "ocaml-re")
265
    (version "1.7.1")
266
    (source (origin
267
              (method url-fetch)
268
              (uri (string-append "https://github.com/ocaml/ocaml-re//archive/"
269
                                  version ".tar.gz"))
270
              (sha256
271
               (base32
272
                "1s3rcr76cgm4p1xmaazc58arkg2lz3zfcp1icm00m6s5ccnkh67b"))))
273
    (build-system ocaml-build-system)
274
    (native-inputs `(("ounit" ,ocaml-ounit)))
275
    (home-page "https://github.com/ocaml/ocaml-re/")
276
    (synopsis "Regular expression library for OCaml")
277
    (description "Pure OCaml regular expressions with:
278
enumerate
279
@item Perl-style regular expressions (module Re_perl)
280
@item Posix extended regular expressions (module Re_posix)
281
@item Emacs-style regular expressions (module Re_emacs)
282
@item Shell-style file globbing (module Re_glob)
283
@item Compatibility layer for OCaml's built-in Str module (module Re_str)
284
@end enumerate")
285
    (license license:expat)))
286
287
(define-public ocaml-ppx-expect
288
  (package
289
    (name "ocaml-ppx-expect")
290
    (version "113.33.03")
291
    (source (janestreet-origin "ppx_expect" version
292
              "03sbs4s5i8l9syr45v25f5hzy7msd2b47k2a9wsq9m43d4imgkrc"))
293
    (build-system ocaml-build-system)
294
    (native-inputs
295
     `(("js-build-tools" ,ocaml-js-build-tools)
296
       ("opam" ,opam)))
297
    (propagated-inputs
298
     `(("fieldslib" ,ocaml-fieldslib)
299
       ("ppx-tools" ,ocaml-ppx-tools)
300
       ("ppx-assert" ,ocaml-ppx-assert)
301
       ("ppx-compare" ,ocaml-ppx-compare)
302
       ("ppx-core" ,ocaml-ppx-core)
303
       ("ppx-custom-printf" ,ocaml-ppx-custom-printf)
304
       ("ppx-driver" ,ocaml-ppx-driver)
305
       ("ppx-fields-conv" ,ocaml-ppx-fields-conv)
306
       ("ppx-inline-test" ,ocaml-ppx-inline-test)
307
       ("ppx-sexp-conv" ,ocaml-ppx-sexp-conv)
308
       ("ppx-variants-conv" ,ocaml-ppx-variants-conv)
309
       ("re" ,ocaml-re)
310
       ("sexplib" ,ocaml-sexplib)
311
       ("variantslib" ,ocaml-variantslib)))
312
    (arguments janestreet-arguments)
313
    (home-page "https://github.com/janestreet/ppx_expect/")
314
    (synopsis "Cram like framework for OCaml")
315
    (description "Expect-test is a framework for writing tests in OCaml, similar
316
to Cram.  Expect-tests mimic the existing inline tests framework with the
317
let%expect_test construct.  The body of an expect-test can contain
318
output-generating code, interleaved with %expect extension expressions to denote
319
the expected output.")
320
    (license license:asl2.0)))
321
322
(define-public ocaml-ppx-jane
323
  (package
324
    (name "ocaml-ppx-jane")
325
    (version "113.33.03")
326
    (source (janestreet-origin "ppx_jane" version
327
              "0bjxkhmzgm6x9dcvjwybbccn34khbvyyjimcbaja30fp6qcqk5yl"))
328
    (build-system ocaml-build-system)
329
    (native-inputs
330
     `(("js-build-tools" ,ocaml-js-build-tools)
331
       ("opam" ,opam)))
332
    (propagated-inputs
333
     `(("ppx-assert" ,ocaml-ppx-assert)
334
       ("ppx-bench" ,ocaml-ppx-bench)
335
       ("ppx-bin-prot" ,ocaml-ppx-bin-prot)
336
       ("ppx-compare" ,ocaml-ppx-compare)
337
       ("ppx-custom-printf" ,ocaml-ppx-custom-printf)
338
       ("ppx-deriving" ,ocaml-ppx-deriving)
339
       ("ppx-enumerate" ,ocaml-ppx-enumerate)
340
       ("ppx-expect" ,ocaml-ppx-expect)
341
       ("ppx-fail" ,ocaml-ppx-fail)
342
       ("ppx-fields-conv" ,ocaml-ppx-fields-conv)
343
       ("ppx-here" ,ocaml-ppx-here)
344
       ("ppx-inline-test" ,ocaml-ppx-inline-test)
345
       ("ppx-let" ,ocaml-ppx-let)
346
       ("ppx-pipebang" ,ocaml-ppx-pipebang)
347
       ("ppx-sexp-conv" ,ocaml-ppx-sexp-conv)
348
       ("ppx-sexp-message" ,ocaml-ppx-sexp-message)
349
       ("ppx-sexp-value" ,ocaml-ppx-sexp-value)
350
       ("ppx-typerep-conv" ,ocaml-ppx-typerep-conv)
351
       ("ppx-variants-conv" ,ocaml-ppx-variants-conv)))
352
    (arguments janestreet-arguments)
353
    (home-page "https://github.com/janestreet/ppx_jane/")
354
    (synopsis "Standard Jane Street ppx rewriters")
355
    (description "Ppx_jane is a ppx_driver including all standard ppx rewriters.")
356
    (license license:asl2.0)))
357
358
(define-public ocaml-core-kernel
359
  (package
360
    (name "ocaml-core-kernel")
361
    (version "113.33.03")
362
    (source (janestreet-origin "core_kernel" version
363
               "0fl23jrwivixawhxinbwaw9cabqnzn7fini7dxpxjjvkxdc8ip5y"))
364
    (native-inputs
365
     `(("js-build-tools" ,ocaml-js-build-tools)
366
       ("ppx-jane" ,ocaml-ppx-jane)
367
       ("opam" ,opam)))
368
    (propagated-inputs
369
     `(("bin_prot" ,ocaml-bin-prot)
370
       ("ppx-assert" ,ocaml-ppx-assert)
371
       ("ppx-bench" ,ocaml-ppx-bench)
372
       ("ppx-driver" ,ocaml-ppx-driver)
373
       ("ppx-expect" ,ocaml-ppx-expect)
374
       ("ppx-inline-test" ,ocaml-ppx-inline-test)
375
       ("typerep" ,ocaml-typerep)
376
       ("sexplib" ,ocaml-sexplib)
377
       ("variantslib" ,ocaml-variantslib)
378
       ("result" ,ocaml-result)
379
       ("fieldslib" ,ocaml-fieldslib)))
380
    (build-system ocaml-build-system)
381
    (arguments janestreet-arguments)
382
    (home-page "https://github.com/janestreet/core_kernel/")
383
    (synopsis "Portable standard library for OCaml")
384
    (description "Core is an alternative to the OCaml standard library.
385
386
Core_kernel is the system-independent part of Core. It is aimed for cases when
387
the full Core is not available, such as in Javascript.")
388
    (license license:asl2.0)))
389
390
(define-public ocaml-async-kernel
391
  (package
392
    (name "ocaml-async-kernel")
393
    (version "113.33.03")
394
    (source (janestreet-origin "async_kernel" version
395
              "04bjsaa23j831r09r38x6xx9nhryvp0z5ihickvhxqa4fb2snyvd"))
396
    (native-inputs
397
     `(("oasis" ,ocaml-oasis)
398
       ("js-build-tools" ,ocaml-js-build-tools)
399
       ("ppx-jane" ,ocaml-ppx-jane)
400
       ("opam" ,opam)))
401
    (propagated-inputs
402
     `(("core-kernel" ,ocaml-core-kernel)))
403
    (build-system ocaml-build-system)
404
    (arguments janestreet-arguments)
405
    (home-page "https://github.com/janestreet/async_kernel/")
406
    (synopsis "Monadic concurrency library")
407
    (description "Monadic concurrency library.")
408
    (license license:asl2.0)))
409
410
(define-public ocaml-async-rpc-kernel
411
  (package
412
    (name "ocaml-async-rpc-kernel")
413
    (version "113.33.03")
414
    (source (janestreet-origin "async_rpc_kernel" version
415
             "0y97h9pkb00v7jpf87m8cbb0ffkclj9g26ph6sq97q8dpisnkjwh"))
416
    (native-inputs
417
     `(("oasis" ,ocaml-oasis)
418
       ("js-build-tools" ,ocaml-js-build-tools)
419
       ("ppx-jane" ,ocaml-ppx-jane)
420
       ("opam" ,opam)))
421
    (propagated-inputs
422
     `(("async-kernel" ,ocaml-async-kernel)))
423
    (build-system ocaml-build-system)
424
    (arguments janestreet-arguments)
425
    (home-page "https://github.com/janestreet/async_rpc_kernel/")
426
    (synopsis "Platform-independent core of Async RPC library")
427
    (description "Platform-independent core of Async RPC library.")
428
    (license license:asl2.0)))
429
430
(define-public ocaml-core
431
  (package
432
    (name "ocaml-core")
433
    (version "113.33.03")
434
    (source (janestreet-origin "core" version
435
              "1znll157qg56g9d3247fjibv1hxv3r9wxgr4nhy19j2vzdh6a268"))
436
    (native-inputs
437
     `(("oasis" ,ocaml-oasis)
438
       ("js-build-tools" ,ocaml-js-build-tools)
439
       ("ppx-jane" ,ocaml-ppx-jane)
440
       ("opam" ,opam)))
441
    (propagated-inputs
442
     `(("core-kernel" ,ocaml-core-kernel)))
443
    (build-system ocaml-build-system)
444
    (arguments janestreet-arguments)
445
    (home-page "https://github.com/janestreet/core/")
446
    (synopsis "Alternative to OCaml's standard library")
447
    (description "The Core suite of libraries is an alternative to OCaml's
448
standard library that was developed by Jane Street.")
449
    (license license:asl2.0)))
450
451
(define-public ocaml-async-unix
452
  (package
453
    (name "ocaml-async-unix")
454
    (version "113.33.03")
455
    (source (janestreet-origin "async_unix" version
456
              "1fwl0lfrizllcfjk8hk8m7lsz9ha2jg6qgk4gssfyz377qvpcq4h"))
457
    (native-inputs
458
     `(("oasis" ,ocaml-oasis)
459
       ("js-build-tools" ,ocaml-js-build-tools)
460
       ("ppx-jane" ,ocaml-ppx-jane)
461
       ("opam" ,opam)))
462
    (propagated-inputs
463
     `(("async-kernel" ,ocaml-async-kernel)
464
       ("core" ,ocaml-core)))
465
    (build-system ocaml-build-system)
466
    (arguments janestreet-arguments)
467
    (home-page "https://github.com/janestreet/async_unix")
468
    (synopsis "Monadic concurrency library")
469
    (description "Monadic concurrency library.")
470
    (license license:asl2.0)))
471
472
(define-public ocaml-async-extra
473
  (package
474
    (name "ocaml-async-extra")
475
    (version "113.33.03")
476
    (source (janestreet-origin "async_extra" version
477
              "1si8jgiq5xh5sl9f2b7f9p17p7zx5h1pg557x2cxywi2x7pxqg4f"))
478
    (native-inputs
479
     `(("oasis" ,ocaml-oasis)
480
       ("js-build-tools" ,ocaml-js-build-tools)
481
       ("ppx-jane" ,ocaml-ppx-jane)
482
       ("opam" ,opam)))
483
    (propagated-inputs
484
     `(("async-rpc-kernel" ,ocaml-async-rpc-kernel)
485
       ("async-unix" ,ocaml-async-unix)
486
       ("core" ,ocaml-core)))
487
    (build-system ocaml-build-system)
488
    (arguments janestreet-arguments)
489
    (home-page "https://github.com/janestreet/async_extra")
490
    (synopsis "Monadic concurrency library")
491
    (description "Monadic concurrency library.")
492
    (license license:asl2.0)))
493
494
(define-public ocaml-async
495
  (package
496
    (name "ocaml-async")
497
    (version "113.33.03")
498
    (source (janestreet-origin "async" version
499
              "0210fyhcs12kpmmd26015bgivkfd2wqkyn3c5wd7688d0f872y25"))
500
    (native-inputs
501
     `(("oasis" ,ocaml-oasis)
502
       ("js-build-tools" ,ocaml-js-build-tools)
503
       ("ppx-jane" ,ocaml-ppx-jane)
504
       ("opam" ,opam)))
505
    (propagated-inputs
506
     `(("async-extra" ,ocaml-async-extra)))
507
    (build-system ocaml-build-system)
508
    (arguments janestreet-arguments)
509
    (home-page "https://github.com/janestreet/async")
510
    (synopsis "Monadic concurrency library")
511
    (description "Monadic concurrency library.")
512
    (license license:asl2.0)))
513
514
(define-public ocaml-ocplib-endian
515
  (package
516
    (name "ocaml-ocplib-endian")
517
    (version "1.0")
518
    (source (origin
519
              (method url-fetch)
520
              (uri (string-append "https://github.com/OCamlPro/ocplib-endian/"
521
                                  "archive/" version ".tar.gz"))
522
              (sha256
523
               (base32
524
                "0hwj09rnzjs0m0kazz5h2mgs6p95j0zlga8cda5srnzqmzhniwkn"))
525
              (file-name (string-append name "-" version ".tar.gz"))))
526
    (build-system ocaml-build-system)
527
    (native-inputs `(("cppo" ,ocaml-cppo)))
528
    (home-page "https://github.com/OCamlPro/ocplib-endian")
529
    (synopsis "Optimised functions to read and write int16/32/64 from strings
530
and bigarrays")
531
    (description "Optimised functions to read and write int16/32/64 from strings
532
and bigarrays, based on new primitives added in version 4.01. It works on
533
strings, bytes and bigstring (Bigarrys of chars), and provides submodules for
534
big- and little-endian, with their unsafe counter-parts.")
535
    (license license:lgpl2.1)))
536
537
(define-public ocaml-cstruct
538
  (package
539
    (name "ocaml-cstruct")
540
    (version "2.3.1")
541
    (source (origin
542
              (method url-fetch)
543
              (uri (string-append "https://github.com/mirage/ocaml-cstruct/"
544
                                  "archive/v" version ".tar.gz"))
545
              (sha256
546
               (base32
547
                "15qpdc8421shq4pprdas9jznpva45229wkfqbwcxw9khaiiz7949"))
548
              (file-name (string-append name "-" version ".tar.gz"))))
549
    (build-system ocaml-build-system)
550
    (arguments
551
     `(#:configure-flags
552
       (list "--enable-lwt" "--enable-async")
553
       #:phases
554
       (modify-phases %standard-phases
555
         (add-after 'install 'link-stubs
556
           (lambda* (#:key outputs #:allow-other-keys)
557
             (let* ((out (assoc-ref outputs "out"))
558
                    (stubs (string-append out "/lib/ocaml/site-lib/stubslibs"))
559
                    (lib (string-append out "/lib/ocaml/site-lib/cstruct")))
560
               (mkdir-p stubs)
561
               (symlink (string-append lib "/dllcstruct_stubs.so")
562
                        (string-append stubs "/dllcstruct_stubs.so"))))))))
563
    (native-inputs
564
     `(("ounit" ,ocaml-ounit)
565
       ("ppx-tools" ,ocaml-ppx-tools)
566
       ("camlp4" ,camlp4)))
567
    (propagated-inputs
568
     `(("ocplib-endian" ,ocaml-ocplib-endian)
569
       ("lwt" ,ocaml-lwt)
570
       ("async" ,ocaml-async)
571
       ("sexplib" ,ocaml-sexplib)))
572
    (home-page "https://github.com/mirage/ocaml-cstruct")
573
    (synopsis "Access C structures via a camlp4 extension")
574
    (description "Cstruct is a library and syntax extension to make it easier
575
to access C-like structures directly from OCaml.  It supports both reading and
576
writing to these structures, and they are accessed via the Bigarray module.")
577
    (license license:isc)))
578
579
(define-public ocaml-hex
580
  (package
581
    (name "ocaml-hex")
582
    (version "1.0.0")
583
    (source (origin
584
              (method url-fetch)
585
              (uri (string-append "https://github.com/mirage/ocaml-hex/"
586
                                  "archive/" version ".tar.gz"))
587
              (sha256
588
               (base32
589
                "0s63g0b8gfv2xm6fv6xg7bva8h76b5pcjb0zw3f8cygs0lq9072v"))
590
              (file-name (string-append name "-" version ".tar.gz"))))
591
    (build-system ocaml-build-system)
592
    (propagated-inputs `(("cstruct" ,ocaml-cstruct)))
593
    (home-page "https://github.com/mirage/ocaml-hex/")
594
    (synopsis "Minimal library providing hexadecimal converters")
595
    (description "Minimal library providing hexadecimal converters.")
596
    (license license:isc)))
597
598
(define-public ocaml-ezjsonm
599
  (package
600
    (name "ocaml-ezjsonm")
601
    (version "0.4.3")
602
    (source (origin
603
              (method url-fetch)
604
              (uri (string-append "https://github.com/mirage/ezjsonm/archive/"
605
                                  version ".tar.gz"))
606
              (sha256
607
               (base32
608
                "1kag0z2xlk4rw73a240dmkxh9rj6psxxcxkm7d7z0rrj6hzjajgq"))
609
              (file-name (string-append name "-" version ".tar.gz"))))
610
    (build-system ocaml-build-system)
611
    (native-inputs
612
     `(("alcotest" ,ocaml-alcotest)))
613
    (propagated-inputs
614
     `(("hex" ,ocaml-hex)
615
       ("jsonm" ,ocaml-jsonm)
616
       ("lwt" ,ocaml-lwt)
617
       ("sexplib" ,ocaml-sexplib)))
618
    (arguments
619
     `(#:configure-flags (list "--enable-lwt")
620
       ;; dllcstruct_stubs.so: cannot open shared object file: No such file
621
       ;; or directory. May be fixed?
622
       #:tests? #f))
623
    (home-page "https://github.com/mirage/ezjsonm/")
624
    (synopsis "An easy interface on top of the Jsonm library")
625
    (description "This version provides more convenient (but far less flexible)
626
input and output functions that go to and from [string] values.  This avoids
627
the need to write signal code, which is useful for quick scripts that
628
manipulate JSON.")
629
    (license license:isc)))
630
631
(define-public ocaml-uri
632
  (package
633
    (name "ocaml-uri")
634
    (version "1.9.2")
635
    (source (origin
636
              (method url-fetch)
637
              (uri (string-append "https://github.com/mirage/ocaml-uri/archive/v"
638
                                  version ".tar.gz"))
639
              (sha256
640
               (base32
641
                "02bzrag79prx261rxf9mlak749pwf4flpfl8p012x1xznv9m0clc"))
642
              (file-name (string-append name "-" version ".tar.gz"))))
643
    (build-system ocaml-build-system)
644
    (native-inputs
645
     `(("ounit" ,ocaml-ounit)))
646
    (propagated-inputs
647
     `(("ppx-sexp-conv" ,ocaml-ppx-sexp-conv)
648
       ("re" ,ocaml-re)
649
       ("ppx-deriving" ,ocaml-ppx-deriving)
650
       ("sexplib" ,ocaml-sexplib)
651
       ("stringext" ,ocaml-stringext)))
652
    (home-page "https://github.com/mirage/ocaml-uri")
653
    (synopsis "RFC3986 URI/URL parsing library")
654
    (description "RFC3986 URI/URL parsing library.")
655
    (license license:isc)))
656
657
(define-public ocaml-easy-format
658
  (package
659
    (name "ocaml-easy-format")
660
    (version "1.2.0")
661
    (source (origin
662
              (method url-fetch)
663
              (uri (string-append "https://github.com/mjambon/easy-format/"
664
                                  "archive/v" version ".tar.gz"))
665
              (sha256
666
               (base32
667
                "1zcz682y9figa84k7lgdjcab5qbzk3yy14ygfqp2dhhrvjygm252"))
668
              (file-name (string-append name "-" version ".tar.gz"))))
669
    (build-system ocaml-build-system)
670
    (arguments
671
     `(#:phases
672
       (modify-phases %standard-phases
673
         (delete 'configure))
674
       #:tests? #f))
675
    (home-page "https://github.com/mjambon/easy-format")
676
    (synopsis "High-level and functional interface to the Format module of the
677
OCaml standard library")
678
    (description "High-level and functional interface to the Format module of
679
the OCaml standard library.")
680
    (license license:bsd-3)))
681
682
(define-public ocaml-optcomp
683
  (package
684
    (name "ocaml-optcomp")
685
    (version "1.6")
686
    (source (origin
687
              (method url-fetch)
688
              (uri (string-append "https://github.com/diml/optcomp/archive/"
689
                                  version ".tar.gz"))
690
              (sha256
691
               (base32
692
                "0hhhb2gisah1h22zlg5iszbgqxdd7x85cwd57bd4mfkx9l7dh8jh"))
693
              (file-name (string-append name "-" version ".tar.gz"))))
694
    (build-system ocaml-build-system)
695
    (arguments
696
     `(#:use-make? #t
697
	   #:make-flags
698
       (list (string-append "BUILDFLAGS=\"-cflags -I,"
699
                            (assoc-ref %build-inputs "camlp4")
700
                            "/lib/ocaml/site-lib/camlp4/Camlp4Parsers\""))))
701
    (native-inputs `(("camlp4" ,camlp4)))
702
    (propagated-inputs `(("camlp4" ,camlp4)))
703
    (home-page "https://github.com/diml/optcomp")
704
    (synopsis "Optional compilation with cpp-like directives")
705
    (description "Optional compilation with cpp-like directives.")
706
    (license license:bsd-3)))
707
708
(define-public ocaml-piqilib
709
  (package
710
    (name "ocaml-piqilib")
711
    (version "0.6.13")
712
    (source (origin
713
              (method url-fetch)
714
              (uri (string-append "https://github.com/alavrik/piqi/archive/v"
715
                                  version ".tar.gz"))
716
              (sha256
717
               (base32
718
                "1whqr2bb3gds2zmrzqnv8vqka9928w4lx6mi6g244kmbwb2h8d8l"))
719
              (file-name (string-append name "-" version ".tar.gz"))
720
              (patches (search-patches "ocaml-piqilib-fix-makefile.patch"))))
721
    (build-system ocaml-build-system)
722
    (arguments
723
     `(#:phases
724
       (modify-phases %standard-phases
725
         (replace 'configure
726
           (lambda* (#:key outputs #:allow-other-keys)
727
             (let ((out (assoc-ref outputs "out")))
728
               (substitute* "make/OCamlMakefile"
729
                 (("/bin/sh") (which "bash")))
730
               (zero? (system* "./configure" "--prefix" out "--ocaml-libdir"
731
                               (string-append out "/lib/ocaml/site-lib"))))))
732
       (add-after 'build 'build-ocaml
733
         (lambda* (#:key outputs #:allow-other-keys)
734
           (zero? (system* "make" "ocaml")))) 
735
       (add-after 'install 'install-ocaml
736
         (lambda* (#:key outputs #:allow-other-keys)
737
           (zero? (system* "make" "ocaml-install"))))
738
       (add-after 'install-ocaml 'link-stubs
739
         (lambda* (#:key outputs #:allow-other-keys)
740
           (let* ((out (assoc-ref outputs "out"))
741
                  (stubs (string-append out "/lib/ocaml/site-lib/stubslibs"))
742
                  (lib (string-append out "/lib/ocaml/site-lib/piqilib")))
743
             (mkdir-p stubs)
744
             (symlink (string-append lib "/dllpiqilib_stubs.so")
745
                      (string-append stubs "/dllpiqilib_stubs.so"))))))))
746
    (native-inputs
747
     `(("which" ,which)
748
       ("camlp4" ,camlp4)))
749
    (propagated-inputs
750
     `(("xmlm" ,ocaml-xmlm)
751
       ("ulex" ,ocaml-ulex)
752
       ("optcomp" ,ocaml-optcomp)
753
       ("easy-format" ,ocaml-easy-format)
754
       ("base64" ,ocaml-base64)))
755
    (home-page "http://piqi.org")
756
    (synopsis "Data serialization and conversion library")
757
    (description "Common library used by piqi command-line tool and piqi-ocaml.")
758
    (license license:asl2.0)))
759
760
(define-public ocaml-uuidm
761
  (package
762
    (name "ocaml-uuidm")
763
    (version "0.9.6")
764
    (source (origin
765
              (method url-fetch)
766
              (uri (string-append "http://erratique.ch/software/uuidm/"
767
                                  "releases/uuidm-" version ".tbz"))
768
              (sha256
769
               (base32
770
                "0hz4fdx0x16k0pw9995vkz5d1hmzz6b16wck9li399rcbfnv5jlc"))))
771
    (build-system ocaml-build-system)
772
    (arguments
773
     `(#:tests? #f
774
       #:build-flags
775
       (list "build" "--with-cmdliner" "true")
776
       #:phases
777
       (modify-phases %standard-phases
778
         (delete 'configure))))
779
    (native-inputs
780
     `(("opam" ,opam)))
781
    (propagated-inputs
782
     `(("cmdliner" ,ocaml-cmdliner)
783
       ("topkg" ,ocaml-topkg)))
784
    (home-page "http://erratique.ch/software/uuidm")
785
    (synopsis "Universally unique identifiers (UUIDs) for OCaml")
786
    (description "Uuidm is an OCaml module implementing 128 bits universally
787
unique identifiers version 3, 5 (named based with MD5, SHA-1 hashing) and 4
788
(random based) according to RFC 4122.")
789
    (license license:isc)))
790
791
(define-public ocamlgraph
792
  (package
793
    (name "ocamlgraph")
794
    (version "1.8.7")
795
    (source (origin
796
              (method url-fetch)
797
              (uri (string-append "http://ocamlgraph.lri.fr/download/"
798
                                  "ocamlgraph-" version ".tar.gz"))
799
              (sha256
800
               (base32
801
                "1845r537swjil2fcj7lgbibc2zybfwqqasrd2s7bncajs83cl1nz"))
802
              (patches (search-patches "ocamlgraph-honor-source-date-epoch.patch"))))
803
    (build-system ocaml-build-system)
804
    (arguments
805
     `(#:install-target "install-findlib"
806
       #:phases
807
       (modify-phases %standard-phases
808
         (add-before 'configure 'fix-/bin/sh
809
           (lambda* (#:key inputs #:allow-other-keys)
810
             (substitute* "configure"
811
               (("-/bin/sh") (string-append "-" (assoc-ref inputs "bash")
812
                                            "/bin/sh"))))))))
813
    (inputs `(("lablgtk" ,lablgtk)))
814
    (home-page "http://ocamlgraph.lri.fr/")
815
    (synopsis "A generic graph library for OCaml")
816
    (description "A generic graph library for OCaml.")
817
    (license license:lgpl2.1)))
818
819
(define-public ocaml-piqi
820
  (package
821
    (name "ocaml-piqi")
822
    (version "0.7.5")
823
    (source (origin
824
              (method url-fetch)
825
              (uri (string-append "https://github.com/alavrik/piqi-ocaml/"
826
                                  "archive/v" version ".tar.gz"))
827
              (sha256
828
               (base32
829
                "0ngz6y8i98i5v2ma8nk6mc83pdsmf2z0ks7m3xi6clfg3zqbddrv"))))
830
    (build-system ocaml-build-system)
831
    (arguments
832
     `(#:make-flags
833
       (list (string-append "DESTDIR=" (assoc-ref %outputs "out")))
834
       #:phases
835
       (modify-phases %standard-phases
836
         (delete 'configure)
837
         (add-before 'build 'patch-/bin/sh
838
           (lambda _
839
             (substitute* "make/OCamlMakefile"
840
               (("/bin/sh") (which "sh")))
841
             #t)))))
842
    (native-inputs
843
     `(("which" ,which)
844
       ("protobuf" ,protobuf))) ; for tests
845
    (propagated-inputs
846
     `(("piqilib" ,ocaml-piqilib)))
847
    (home-page "https://github.com/alavrik/piqi-ocaml")
848
    (synopsis "Protocol serialization system for OCaml")
849
    (description "Piqi is a multi-format data serialization system for OCaml.
850
It provides a uniform interface for serializing OCaml data structures to JSON,
851
XML and Protocol Buffers formats.")
852
    (license license:asl2.0)))
853
854
(define-public bap
855
  (package
856
    (name "bap")
857
    (version "1.1.0")
858
    (home-page "https://github.com/BinaryAnalysisPlatform/bap")
859
    (source (origin
860
              (method url-fetch)
861
              (uri (string-append home-page "/archive/v" version ".tar.gz"))
862
              (sha256
863
               (base32
864
                "1ms95m4j1qrmy7zqmsn2izh7gq68lnmssl7chyhk977kd3sxj66m"))
865
              (file-name (string-append name "-" version ".tar.gz"))))
866
   (build-system ocaml-build-system)
867
   (native-inputs
868
    `(("oasis" ,ocaml-oasis)
869
      ("clang" ,clang)
870
      ("ounit" ,ocaml-ounit)))
871
   (propagated-inputs
872
    `(("core-kernel" ,ocaml-core-kernel)
873
      ("ppx-driver" ,ocaml-ppx-driver)
874
      ("uri" ,ocaml-uri)
875
      ("llvm" ,llvm)
876
      ("gmp" ,gmp)
877
      ("clang-runtime" ,clang-runtime)
878
      ("fileutils" ,ocaml-fileutils)
879
      ("cmdliner" ,ocaml-cmdliner)
880
      ("zarith" ,ocaml-zarith)
881
      ("uuidm" ,ocaml-uuidm)
882
      ("camlzip" ,camlzip)
883
      ("frontc" ,ocaml-frontc)
884
      ("ezjsonm" ,ocaml-ezjsonm)
885
      ("ocurl" ,ocaml-ocurl)
886
      ("piqi" ,ocaml-piqi)
887
      ("ocamlgraph" ,ocamlgraph)
888
      ("bitstring" ,ocaml-bitstring)
889
      ("ppx-jane" ,ocaml-ppx-jane)
890
      ("re" ,ocaml-re)))
891
   (inputs `(("llvm" ,llvm)))
892
   (arguments
893
    `(#:use-make? #t
894
      #:phases
895
      (modify-phases %standard-phases
896
        (replace 'configure
897
          (lambda* (#:key outputs #:allow-other-keys)
898
            (zero? (system* "./configure" "--prefix"
899
                            (assoc-ref outputs "out")
900
                            "--libdir"
901
                            (string-append
902
                              (assoc-ref outputs "out")
903
                              "/lib/ocaml/site-lib")
904
                            "--with-llvm-version=3.8"
905
                            "--with-llvm-config=llvm-config"
906
                            "--enable-everything"))))
907
        (add-before 'install 'fix-ocamlpath
908
          (lambda* (#:key outputs #:allow-other-keys)
909
            (setenv "OCAMLPATH"
910
                    (string-append
911
                      (getenv "OCAMLPATH") ":"
912
                      (assoc-ref outputs "out")
913
                      "/lib/ocaml/site-lib"))
914
            (setenv "PATH"
915
                    (string-append (getenv "PATH") ":"
916
                                   (assoc-ref outputs "out") "/bin"))))
917
        (add-after 'install 'link-stubs
918
          (lambda* (#:key outputs #:allow-other-keys)
919
            (let* ((out (assoc-ref outputs "out"))
920
                   (stubs (string-append out "/lib/ocaml/site-lib/stubslibs"))
921
                   (lib (string-append out "/lib/ocaml/site-lib/bap-plugin-llvm")))
922
              (mkdir-p stubs)
923
              (symlink (string-append lib "/dllllvm_plugin_stubs.so")
924
                       (string-append stubs "/dllllvm_plugin_stubs.so"))))))))
925
   (synopsis "Binary Analysis Platform")
926
   (description "Binary Analysis Platform is a framework for writing program
927
analysis tools, that target binary files.  The framework consists of a plethora
928
of libraries, plugins, and frontends.  The libraries provide code reusability,
929
the plugins facilitate extensibility, and the frontends serve as entry points.")
930
   (license license:expat)))
931
932
(define-public ocaml-camomile
933
  (package
934
    (name "ocaml-camomile")
935
    (version "0.8.5")
936
    (home-page "https://github.com/yoriyuki/Camomile")
937
    (source (origin
938
              (method url-fetch)
939
              (uri (string-append home-page "/releases/download/rel-" version
940
                                  "/camomile-" version ".tar.bz2"))
941
              (sha256
942
               (base32
943
                "003ikpvpaliy5hblhckfmln34zqz0mk3y2m1fqvbjngh3h2np045"))))
944
    (build-system ocaml-build-system)
945
    (native-inputs `(("camlp4" ,camlp4)))
946
    (arguments
947
     `(#:phases
948
       (modify-phases %standard-phases
949
         (add-before 'configure 'fix-bin/sh
950
           (lambda* (#:key #:allow-other-keys)
951
             (substitute* "configure"
952
               (("CONFIG_SHELL-/bin/sh")
953
                (string-append "CONFIG_SHELL-" (which "bash")))))))))
954
    (synopsis "Comprehensive Unicode library")
955
    (description "Camomile is a Unicode library for OCaml.  Camomile provides
956
Unicode character type, UTF-8, UTF-16, UTF-32 strings, conversion to/from about
957
200 encodings, collation and locale-sensitive case mappings, and more.  The
958
library is currently designed for Unicode Standard 3.2.")
959
    (license license:lgpl2.0+))) ; with an exception
960
961
(define-public ocaml-zed
962
  (package
963
    (name "ocaml-zed")
964
    (version "1.4")
965
    (source (origin
966
              (method url-fetch)
967
              (uri (string-append "https://github.com/diml/zed/archive/"
968
                                  version ".tar.gz"))
969
              (sha256
970
               (base32
971
                "0pvfq9ikhbkv4ksn3k3vzs6wiwkihjav3n81lhxm54z9931gfwnz"))))
972
    (build-system ocaml-build-system)
973
    (propagated-inputs
974
     `(("camomile" ,ocaml-camomile)
975
       ("react" ,ocaml-react)))
976
    (home-page "https://github.com/diml/zed")
977
    (synopsis "Abstract engine for text edition in OCaml")
978
    (description "Zed is an abstract engine for text edition. It can be used to
979
write text editors, edition widgets, readlines, ...
980
981
Zed uses Camomile to fully support the Unicode specification, and implements an
982
UTF-8 encoded string type with validation, and a rope datastructure to achieve
983
efficient operations on large Unicode buffers. Zed also features a regular
984
expression search on ropes.
985
986
To support efficient text edition capabilities, Zed provides macro recording
987
and cursor management facilities.")
988
    (license license:bsd-3)))
989
990
(define-public ocaml-lambda-term
991
  (package
992
    (name "ocaml-lambda-term")
993
    (version "1.10.1")
994
    (home-page "https://github.com/diml/lambda-term")
995
    (source (origin
996
              (method url-fetch)
997
              (uri (string-append home-page "/archive/" version ".tar.gz"))
998
              (sha256
999
               (base32
1000
                "1449glcsavcwbcsxbd7wcjz50y8vvin4zwpmkhq8i6jca3f3sknj"))))
1001
    (build-system ocaml-build-system)
1002
    (propagated-inputs
1003
     `(("zed" ,ocaml-zed)
1004
       ("lwt" ,ocaml-lwt)
1005
       ("react" ,ocaml-react)))
1006
    (arguments
1007
     `(#:phases
1008
       (modify-phases %standard-phases
1009
        (add-after 'install 'link-stubs
1010
          (lambda* (#:key outputs #:allow-other-keys)
1011
            (let* ((out (assoc-ref outputs "out"))
1012
                   (stubs (string-append out "/lib/ocaml/site-lib/stubslibs"))
1013
                   (lib (string-append out "/lib/ocaml/site-lib/lambda-term")))
1014
              (mkdir-p stubs)
1015
              (symlink (string-append lib "/dlllambda-term_stubs.so")
1016
                       (string-append stubs "/dlllambda-term_stubs.so"))))))))
1017
    (synopsis "Terminal manipulation library for OCaml")
1018
    (description "Lambda-term is a cross-platform library for manipulating the
1019
terminal. It provides an abstraction for keys, mouse events, colors, as well as
1020
a set of widgets to write curses-like applications.
1021
1022
The main objective of lambda-term is to provide a higher level functional
1023
interface to terminal manipulation than, for example, ncurses, by providing a
1024
native OCaml interface instead of bindings to a C library.
1025
1026
Lambda-term integrates with zed to provide text edition facilities in console
1027
applications.")
1028
    (license license:bsd-3)))
1029
1030
(define-public ocaml-utop
1031
  (package
1032
    (name "ocaml-utop")
1033
    (version "1.19.3")
1034
    (source (origin
1035
              (method url-fetch)
1036
              (uri (string-append "https://github.com/diml/utop/archive/"
1037
                                  version ".tar.gz"))
1038
              (file-name (string-append name "-" version ".tar.gz"))
1039
              (sha256
1040
               (base32
1041
                "16z02vp9n97iax4fqpbi7v86r75vbabxvnd1rirh8w2miixs1g4x"))))
1042
    (build-system ocaml-build-system)
1043
    (native-inputs
1044
     `(("cppo" ,ocaml-cppo)))
1045
    (propagated-inputs
1046
     `(("lambda-term" ,ocaml-lambda-term)
1047
       ("lwt" ,ocaml-lwt)
1048
       ("react" ,ocaml-react)))
1049
    (home-page "https://github.com/diml/utop")
1050
    (synopsis "Universal toplevel for OCaml")
1051
    (description "utop is an improved toplevel for OCaml.  It can run in a
1052
terminal or in Emacs.  It supports line edition, history, real-time and context
1053
sensitive completion, colors, and more.
1054
1055
It integrates with the tuareg mode in Emacs.")
1056
    (license license:bsd-3)))
1057
1058
(define-public proof-general2
1059
  (package
1060
    (name "proof-general2")
1061
    (version "4.4")
1062
    (source (origin
1063
              (method url-fetch)
1064
              (uri (string-append
1065
                    "https://github.com/ProofGeneral/PG/archive/v"
1066
                    version ".tar.gz"))
1067
              (file-name (string-append name "-" version ".tar.gz"))
1068
              (sha256
1069
               (base32
1070
                "0zif2fv6mm4pv75nh10q3p37n293495rvx470bx7ma382zc3d8hv"))))
1071
    (build-system gnu-build-system)
1072
    (native-inputs
1073
     `(("which" ,which)
1074
       ("emacs" ,emacs-minimal)
1075
       ("texinfo" ,texinfo)))
1076
    (inputs
1077
     `(("host-emacs" ,emacs)
1078
       ("perl" ,perl)
1079
       ("coq" ,coq)))
1080
    (arguments
1081
     `(#:tests? #f  ; no check target
1082
       #:make-flags (list (string-append "PREFIX=" %output)
1083
                          (string-append "DEST_PREFIX=" %output)
1084
                          "-j1")
1085
       #:modules ((guix build gnu-build-system)
1086
                  (guix build utils)
1087
                  (guix build emacs-utils))
1088
       #:imported-modules (,@%gnu-build-system-modules
1089
                           (guix build emacs-utils))
1090
       #:phases
1091
       (modify-phases %standard-phases
1092
         (delete 'configure)
1093
         (add-after 'unpack 'disable-byte-compile-error-on-warn
1094
                    (lambda _
1095
                      (substitute* "Makefile"
1096
                        (("\\(setq byte-compile-error-on-warn t\\)")
1097
                         "(setq byte-compile-error-on-warn nil)"))
1098
                      #t))
1099
         (add-after 'unpack 'patch-hardcoded-paths
1100
                    (lambda* (#:key inputs outputs #:allow-other-keys)
1101
                      (let ((out   (assoc-ref outputs "out"))
1102
                            (coq   (assoc-ref inputs "coq"))
1103
                            (emacs (assoc-ref inputs "host-emacs")))
1104
                        (define (coq-prog name)
1105
                          (string-append coq "/bin/" name))
1106
                        (substitute* "pgshell/pgshell.el"
1107
                          (("/bin/sh") (which "sh")))
1108
                        ;(emacs-substitute-variables "coq/coq.el"
1109
                        ;  ("coq-prog-name"           (coq-prog "coqtop"))
1110
                        ;  ("coq-compiler"            (coq-prog "coqc"))
1111
                        ;  ("coq-dependency-analyzer" (coq-prog "coqdep")))
1112
                        (substitute* "Makefile"
1113
                          (("/sbin/install-info") "install-info"))
1114
                        (substitute* "bin/proofgeneral"
1115
                          (("^PGHOMEDEFAULT=.*" all)
1116
                           (string-append all
1117
                                          "PGHOME=$PGHOMEDEFAULT\n"
1118
                                          "EMACS=" emacs "/bin/emacs")))
1119
                        #t))))))
1120
         ;(add-after 'unpack 'clean
1121
         ;           (lambda _
1122
         ;             ;; Delete the pre-compiled elc files for Emacs 23.
1123
         ;             (zero? (system* "make" "clean"))))
1124
         ;(add-after 'install 'install-doc
1125
         ;           (lambda* (#:key make-flags #:allow-other-keys)
1126
         ;             ;; XXX FIXME avoid building/installing pdf files,
1127
         ;             ;; due to unresolved errors building them.
1128
         ;             (substitute* "Makefile"
1129
         ;               ((" [^ ]*\\.pdf") ""))
1130
         ;             (zero? (apply system* "make" "install-doc"
1131
         ;                           make-flags)))))))
1132
    (home-page "http://proofgeneral.inf.ed.ac.uk/")
1133
    (synopsis "Generic front-end for proof assistants based on Emacs")
1134
    (description
1135
     "Proof General is a major mode to turn Emacs into an interactive proof
1136
assistant to write formal mathematical proofs using a variety of theorem
1137
provers.")
1138
    (license license:gpl2+)))
1139
1140
(define-public compcert
1141
  (package
1142
    (name "compcert")
1143
    (version "3.0")
1144
    (source (origin
1145
              (method url-fetch)
1146
              (uri (string-append "http://compcert.inria.fr/release/compcert-"
1147
                                  version ".tgz"))
1148
              (sha256
1149
               (base32
1150
                "03fxf01acvy0akzb1czk33jsfmv2rka0m0jc1a2gmzs9i192rr7m"))))
1151
    (build-system gnu-build-system)
1152
    (arguments
1153
     `(#:phases
1154
       (modify-phases %standard-phases
1155
         (replace 'configure
1156
           (lambda* (#:key outputs #:allow-other-keys)
1157
             (zero? (system* "./configure" "x86_64-linux" "-prefix"
1158
                             (assoc-ref outputs "out"))))))
1159
       #:tests? #f))
1160
    (native-inputs
1161
     `(("ocaml" ,ocaml)
1162
       ("coq" ,coq)))
1163
    (inputs
1164
     `(("menhir" ,ocaml-menhir)))
1165
    (home-page "http://compcert.inria.fr")
1166
    (synopsis "Certified C compiler")
1167
    (description "CompCert is a certified (with coq) C compiler.  Warning: this
1168
package is not free software!")
1169
    ;; actually the "INRIA Non-Commercial License Agreement"
1170
    ;; a non-free license.
1171
    (license (license:non-copyleft "file:///LICENSE"))))
1172
1173
;; yet another build system <3
1174
;; In this one, the autoconf-generated configure script configures the build and
1175
;; builds remake from source, a make-like system specific to this package.
1176
(define-public coq-flocq
1177
  (package
1178
    (name "coq-flocq")
1179
    (version "2.5.2")
1180
    (source (origin
1181
              (method url-fetch)
1182
              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36199/flocq-"
1183
                                  version ".tar.gz"))
1184
              (sha256
1185
               (base32
1186
                "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h"))))
1187
    (build-system gnu-build-system)
1188
    (native-inputs
1189
     `(("ocaml" ,ocaml)
1190
       ("which" ,which)
1191
       ("coq" ,coq)))
1192
    (arguments
1193
     `(#:configure-flags
1194
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
1195
                            "/lib/coq/user-contrib/Flocq"))
1196
       #:phases
1197
       (modify-phases %standard-phases
1198
         (add-before 'configure 'fix-remake
1199
           (lambda _
1200
             (substitute* "remake.cpp"
1201
               (("/bin/sh") (which "sh")))))
1202
         (replace 'build
1203
           (lambda _
1204
             (zero? (system* "./remake"))))
1205
         (replace 'check
1206
           (lambda _
1207
             (zero? (system* "./remake" "check"))))
1208
             ;; TODO: requires coq-gappa and coq-interval.
1209
             ;(zero? (system* "./remake" "check-more"))))
1210
         (replace 'install
1211
           (lambda _
1212
             (zero? (system* "./remake" "install")))))))
1213
    (home-page "http://flocq.gforge.inria.fr/")
1214
    (synopsis "Floating-point formalization for the Coq system")
1215
    (description "Flocq (Floats for Coq) is a floating-point formalization for
1216
the Coq system.  It provides a comprehensive library of theorems on a multi-radix
1217
multi-precision arithmetic.  It also supports efficient numerical computations
1218
inside Coq.")
1219
    (license license:lgpl3+)))
1220
1221
(define-public coq-gappa
1222
  (package
1223
    (name "coq-gappa")
1224
    (version "1.3.1")
1225
    (source (origin
1226
              (method url-fetch)
1227
              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36351/gappa-"
1228
                                  version ".tar.gz"))
1229
              (sha256
1230
               (base32
1231
                "0924jr6f15fx22qfsvim5vc0qxqg30ivg9zxj34lf6slbgdl3j39"))))
1232
    (build-system gnu-build-system)
1233
    (native-inputs
1234
     `(("ocaml" ,ocaml)
1235
       ("which" ,which)
1236
       ("coq" ,coq)
1237
       ("bison" ,bison)
1238
       ("flex" ,flex)))
1239
    (inputs
1240
     `(("gmp" ,gmp)
1241
       ("mpfr" ,mpfr)
1242
       ("boost" ,boost)))
1243
    (arguments
1244
     `(#:configure-flags
1245
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
1246
                            "/lib/coq/user-contrib/Gappa"))
1247
       #:phases
1248
       (modify-phases %standard-phases
1249
         (add-before 'configure 'fix-remake
1250
           (lambda _
1251
             (substitute* "remake.cpp"
1252
               (("/bin/sh") (which "sh")))))
1253
         (replace 'build
1254
           (lambda _
1255
             (zero? (system* "./remake"))))
1256
         (replace 'check
1257
           (lambda _
1258
             (zero? (system* "./remake" "check"))))
1259
         (replace 'install
1260
           (lambda _
1261
             (zero? (system* "./remake" "install")))))))
1262
    (home-page "http://gappa.gforge.inria.fr/")
1263
    (synopsis "Verify and formally prove properties on numerical programs")
1264
    (description "Gappa is a tool intended to help verifying and formally proving
1265
properties on numerical programs dealing with floating-point or fixed-point
1266
arithmetic.  It has been used to write robust floating-point filters for CGAL
1267
and it is used to certify elementary functions in CRlibm.  While Gappa is
1268
intended to be used directly, it can also act as a backend prover for the Why3
1269
software verification plateform or as an automatic tactic for the Coq proof
1270
assistant.")
1271
    (license (list license:gpl2 license:cecill))))
1272
1273
(define-public coq-mathcomp
1274
  (package
1275
    (name "coq-mathcomp")
1276
    (version "1.6.1")
1277
    (source (origin
1278
              (method url-fetch)
1279
              (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
1280
                                  version ".tar.gz"))
1281
              (sha256
1282
               (base32
1283
                "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw"))))
1284
    (build-system gnu-build-system)
1285
    (native-inputs
1286
     `(("ocaml" ,ocaml)
1287
       ("which" ,which)
1288
       ("coq" ,coq)))
1289
    (arguments
1290
     `(#:tests? #f; No need to test formally-verified programs :)
1291
       #:phases
1292
       (modify-phases %standard-phases
1293
         (delete 'configure)
1294
         (add-before 'build 'chdir
1295
           (lambda _
1296
             (chdir "mathcomp")))
1297
         (replace 'install
1298
           (lambda* (#:key outputs #:allow-other-keys)
1299
             (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
1300
             (zero? (system* "make" "-f" "Makefile.coq"
1301
                             (string-append "COQLIB=" (assoc-ref outputs "out")
1302
                                            "/lib/coq/")
1303
                             "install")))))))
1304
    (home-page "https://math-comp.github.io/math-comp/")
1305
    (synopsis "Mathematical Components for Coq")
1306
    (description "Mathematical Components for Coq has its origins in the formal
1307
proof of the Four Colour Theorem.  Since then it has grown to cover many areas
1308
of mathematics and has been used for large scale projects like the formal proof
1309
of the Odd Order Theorem.
1310
1311
The library is written using the Ssreflect proof language that is an integral
1312
part of the distribution.")
1313
    (license license:cecill-b)))
1314
1315
;; TODO: coquelicot
1316
1317
(define-public coq-interval
1318
  (package
1319
    (name "coq-interval")
1320
    (version "3.2.0")
1321
    (source (origin
1322
              (method url-fetch)
1323
              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
1324
                                  "file/36538/interval-" version ".tar.gz"))
1325
              (sha256
1326
               (base32
1327
                "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3"))))
1328
    (build-system gnu-build-system)
1329
    (native-inputs
1330
     `(("ocaml" ,ocaml)
1331
       ("which" ,which)
1332
       ("coq" ,coq)))
1333
    (propagated-inputs
1334
     `(("flocq" ,coq-flocq)
1335
       ("mathcomp" ,coq-mathcomp)))
1336
    (arguments
1337
     `(#:configure-flags
1338
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
1339
                            "/lib/coq/user-contrib/Gappa"))
1340
       #:phases
1341
       (modify-phases %standard-phases
1342
         (add-before 'configure 'fix-remake
1343
           (lambda _
1344
             (substitute* "remake.cpp"
1345
               (("/bin/sh") (which "sh")))))
1346
         (replace 'build
1347
           (lambda _
1348
             (zero? (system* "./remake"))))
1349
         (replace 'check
1350
           (lambda _
1351
             (zero? (system* "./remake" "check"))))
1352
         (replace 'install
1353
           (lambda _
1354
             (zero? (system* "./remake" "install")))))))
1355
    (home-page "http://coq-interval.gforge.inria.fr/")
1356
    (synopsis "Coq tactics to simplify inequality proofs")
1357
    (description "Interval provides vernacular files containing tactics for
1358
simplifying the proofs of inequalities on expressions of real numbers for the
1359
Coq proof assistant.")
1360
    (license license:cecill-c)))
1361