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 git-download)
23
  #:use-module (guix utils)
24
  #:use-module (guix build-system gnu)
25
  #:use-module (guix build-system ocaml)
26
  #:use-module ((guix licenses) #:prefix license:)
27
  #:use-module (gnu packages)
28
  #:use-module (gnu packages assembly)
29
  #:use-module (gnu packages autotools)
30
  #:use-module (gnu packages base)
31
  #:use-module (gnu packages bison)
32
  #:use-module (gnu packages boost)
33
  #:use-module (gnu packages check)
34
  #:use-module (gnu packages emacs)
35
  #:use-module (gnu packages flex)
36
  #:use-module (gnu packages llvm)
37
  #:use-module (gnu packages m4)
38
  #:use-module (gnu packages maths)
39
  #:use-module (gnu packages multiprecision)
40
  #:use-module (gnu packages ocaml)
41
  #:use-module (gnu packages perl)
42
  #:use-module (gnu packages pkg-config)
43
  #:use-module (gnu packages protobuf)
44
  #:use-module (gnu packages python)
45
  #:use-module (gnu packages tex)
46
  #:use-module (gnu packages texinfo)
47
  #:use-module (more packages smt)
48
  #:use-module (ice-9 match))
49
50
(define (ocaml-forge-uri name version file-number)
51
  (string-append "https://forge.ocamlcore.org/frs/download.php/"
52
                 (number->string file-number) "/" name "-" version
53
                 ".tar.gz"))
54
55
(define-public proof-general2
56
  (package
57
    (name "proof-general2")
58
    (version "4.4")
59
    (source (origin
60
              (method url-fetch)
61
              (uri (string-append
62
                    "https://github.com/ProofGeneral/PG/archive/v"
63
                    version ".tar.gz"))
64
              (file-name (string-append name "-" version ".tar.gz"))
65
              (sha256
66
               (base32
67
                "0zif2fv6mm4pv75nh10q3p37n293495rvx470bx7ma382zc3d8hv"))))
68
    (build-system gnu-build-system)
69
    (native-inputs
70
     `(("which" ,which)
71
       ("emacs" ,emacs-minimal)
72
       ("texinfo" ,texinfo)))
73
    (inputs
74
     `(("host-emacs" ,emacs)
75
       ("perl" ,perl)
76
       ("coq" ,coq)))
77
    (arguments
78
     `(#:tests? #f  ; no check target
79
       #:make-flags (list (string-append "PREFIX=" %output)
80
                          (string-append "DEST_PREFIX=" %output)
81
                          "-j1")
82
       #:modules ((guix build gnu-build-system)
83
                  (guix build utils)
84
                  (guix build emacs-utils))
85
       #:imported-modules (,@%gnu-build-system-modules
86
                           (guix build emacs-utils))
87
       #:phases
88
       (modify-phases %standard-phases
89
         (delete 'configure)
90
         (add-after 'unpack 'disable-byte-compile-error-on-warn
91
                    (lambda _
92
                      (substitute* "Makefile"
93
                        (("\\(setq byte-compile-error-on-warn t\\)")
94
                         "(setq byte-compile-error-on-warn nil)"))
95
                      #t))
96
         (add-after 'unpack 'patch-hardcoded-paths
97
                    (lambda* (#:key inputs outputs #:allow-other-keys)
98
                      (let ((out   (assoc-ref outputs "out"))
99
                            (coq   (assoc-ref inputs "coq"))
100
                            (emacs (assoc-ref inputs "host-emacs")))
101
                        (define (coq-prog name)
102
                          (string-append coq "/bin/" name))
103
                        (substitute* "pgshell/pgshell.el"
104
                          (("/bin/sh") (which "sh")))
105
                        ;(emacs-substitute-variables "coq/coq.el"
106
                        ;  ("coq-prog-name"           (coq-prog "coqtop"))
107
                        ;  ("coq-compiler"            (coq-prog "coqc"))
108
                        ;  ("coq-dependency-analyzer" (coq-prog "coqdep")))
109
                        (substitute* "Makefile"
110
                          (("/sbin/install-info") "install-info"))
111
                        (substitute* "bin/proofgeneral"
112
                          (("^PGHOMEDEFAULT=.*" all)
113
                           (string-append all
114
                                          "PGHOME=$PGHOMEDEFAULT\n"
115
                                          "EMACS=" emacs "/bin/emacs")))
116
                        #t))))))
117
         ;(add-after 'unpack 'clean
118
         ;           (lambda _
119
         ;             ;; Delete the pre-compiled elc files for Emacs 23.
120
         ;             (zero? (system* "make" "clean"))))
121
         ;(add-after 'install 'install-doc
122
         ;           (lambda* (#:key make-flags #:allow-other-keys)
123
         ;             ;; XXX FIXME avoid building/installing pdf files,
124
         ;             ;; due to unresolved errors building them.
125
         ;             (substitute* "Makefile"
126
         ;               ((" [^ ]*\\.pdf") ""))
127
         ;             (zero? (apply system* "make" "install-doc"
128
         ;                           make-flags)))))))
129
    (home-page "http://proofgeneral.inf.ed.ac.uk/")
130
    (synopsis "Generic front-end for proof assistants based on Emacs")
131
    (description
132
     "Proof General is a major mode to turn Emacs into an interactive proof
133
assistant to write formal mathematical proofs using a variety of theorem
134
provers.")
135
    (license license:gpl2+)))
136
137
(define-public coq-8.6
138
  (package
139
    (inherit coq)
140
    (name "coq")
141
    (version "8.6.1")
142
    (source (origin
143
              (method url-fetch)
144
              (uri (string-append "https://github.com/coq/coq/archive/V"
145
                                  version ".tar.gz"))
146
              (file-name (string-append name "-" version ".tar.gz"))
147
              (sha256
148
               (base32
149
                "02nm5sn79hrb9fdmkhyclk80jydadf4jcafmr3idwr5h4z56qbms"))))
150
    (arguments
151
     `(#:phases
152
       (modify-phases %standard-phases
153
         (replace 'configure
154
           (lambda* (#:key outputs #:allow-other-keys)
155
             (let* ((out (assoc-ref outputs "out"))
156
                    (mandir (string-append out "/share/man"))
157
                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
158
               (invoke "./configure"
159
                       "-prefix" out
160
                       "-mandir" mandir
161
                       "-browser" browser
162
                       "-coqide" "opt"))
163
             #t))
164
         (replace 'build
165
           (lambda* (#:key inputs #:allow-other-keys)
166
             (substitute* "ide/ideutils.ml"
167
               (("Bytes.unsafe_to_string read_string") "read_string"))
168
             (invoke "make" "-j" (number->string
169
                                  (parallel-job-count))
170
                     (string-append
171
                       "USERFLAGS=-I "
172
                       (assoc-ref inputs "ocaml-num")
173
                       "/lib/ocaml/site-lib")
174
                     "world")
175
             #t))
176
         (delete 'check)
177
         (add-after 'install 'check
178
           (lambda _
179
             (with-directory-excursion "test-suite"
180
               (invoke "make"))
181
             #t)))))))
182
183
(define-public coq-8.7
184
  (package
185
    (inherit coq)
186
    (name "coq")
187
    (version "8.7.2")
188
    (source (origin
189
              (method url-fetch)
190
              (uri (string-append "https://github.com/coq/coq/archive/V"
191
                                  version ".tar.gz"))
192
              (file-name (string-append name "-" version ".tar.gz"))
193
              (sha256
194
               (base32
195
                "1lkqvs7ayzv5kkg26y837pg0d6r2b5hbjxl71ba93f39kybw69gg"))))
196
    (arguments
197
     `(#:phases
198
       (modify-phases %standard-phases
199
         (replace 'configure
200
           (lambda* (#:key outputs #:allow-other-keys)
201
             (let* ((out (assoc-ref outputs "out"))
202
                    (mandir (string-append out "/share/man"))
203
                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
204
               (invoke "./configure"
205
                       "-prefix" out
206
                       "-mandir" mandir
207
                       "-browser" browser
208
                       "-coqide" "opt"))
209
             #t))
210
         (replace 'build
211
           (lambda* (#:key inputs #:allow-other-keys)
212
             (substitute* "ide/ideutils.ml"
213
               (("Bytes.unsafe_to_string read_string") "read_string"))
214
             (invoke "make" "-j" (number->string
215
                                  (parallel-job-count))
216
                     (string-append
217
                       "USERFLAGS=-I "
218
                       (assoc-ref inputs "ocaml-num")
219
                       "/lib/ocaml/site-lib")
220
                     "world")
221
             #t))
222
         (delete 'check)
223
         (add-after 'install 'check
224
           (lambda _
225
             (with-directory-excursion "test-suite"
226
               ;; These two tests fail.
227
               ;; This one fails because the output is not formatted as expected.
228
               (delete-file-recursively "coq-makefile/timing")
229
               ;; This one fails because we didn't build coqtop.byte.
230
               (delete-file-recursively "coq-makefile/findlib-package")
231
               (invoke "make"))
232
             #t)))))))
233
234
(define-public coq-bignums-8.7
235
  (package
236
    (inherit coq-bignums)
237
    (name "coq-bignums")
238
    (version "8.7.0")
239
    (source (origin
240
              (method url-fetch)
241
              (uri (string-append "https://github.com/coq/bignums/archive/V"
242
                                  version ".tar.gz"))
243
              (file-name (string-append name "-" version ".tar.gz"))
244
              (sha256
245
               (base32
246
                "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx"))))
247
    (native-inputs
248
     `(("ocaml" ,ocaml)
249
       ("coq-8.7" ,coq-8.7)))
250
    (inputs
251
     `(("camlp5" ,camlp5)))))
252
253
(define-public ppsimpl
254
  (package
255
    (name "ppsimpl")
256
    (version "8.7")
257
    (source (origin
258
              (method git-fetch)
259
              (uri (git-reference
260
                     (url "https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git")
261
                     (commit "86255a47568df58767d1d8e0b9e2da31cf73a5fc")))
262
              (file-name (string-append name "-" version))
263
              (sha256
264
               (base32
265
                "0h509w43j2wd2pyx04k3xfd0bsbmqscwqvhf8whzc3cxzl4j6vvq"))))
266
              ;(uri "https://gforge.inria.fr/frs/download.php/file/37615/ppsimpl-09-07-2018.tar.gz")
267
              ;(sha256
268
              ; (base32
269
              ;  "010zgskc1wd5v6wmmyxaapvwxjlgbdqqiks2dvf6llx03b07ak59"))))
270
    (build-system gnu-build-system)
271
    (arguments
272
     `(#:test-target "test"
273
       #:configure-flags
274
       (list "-R" (string-append (assoc-ref %build-inputs "compcert") "/lib/coq/user-contrib/compcert") "compcert")
275
       #:make-flags (list "COQC=coqc -R src PP -I src"
276
                          (string-append
277
                            "COQLIBINSTALL="
278
                            (assoc-ref %outputs "out")
279
                            "/lib/coq/user-contrib"))))
280
    (inputs
281
     `(("coq-bignums-8.7" ,coq-bignums-8.7)
282
       ("compcert" ,compcert)))
283
    (native-inputs
284
     `(("coq-8.7" ,coq-8.7)
285
       ("ocaml" ,ocaml)
286
       ("ocaml-findlib" ,ocaml-findlib)
287
       ("camlp4" ,camlp4)
288
       ("camlp5" ,camlp5)
289
       ("which" ,which)))
290
    (home-page "")
291
    (synopsis "")
292
    (description "")
293
    ;; No declared license -> all rights reserved
294
    (license #f)))
295
296
(define-public compcert
297
  (package
298
    (name "compcert")
299
    (version "3.3")
300
    (source (origin
301
              (method url-fetch)
302
              (uri (string-append "http://compcert.inria.fr/release/compcert-"
303
                                  version ".tgz"))
304
              (sha256
305
               (base32
306
                "16xrqcwak1v1fk5ndx6jf1yvxv3adsr7p7z34gfm2mpggxnq0xwn"))))
307
    (build-system gnu-build-system)
308
    (arguments
309
     `(#:phases
310
       (modify-phases %standard-phases
311
         (replace 'configure
312
           (lambda* (#:key outputs #:allow-other-keys)
313
             (let ((system ,(match (or (%current-target-system) (%current-system))
314
                              ("x86_64-linux" "x86_64-linux")
315
                              ("i686-linux" "x86_32-linux")
316
                              ("armhf-linux" "arm-linux"))))
317
               (format #t "Building for ~a~%" system)
318
               (invoke "./configure" system "-prefix"
319
                       (assoc-ref outputs "out")))
320
             #t))
321
         (add-after 'install 'install-lib
322
           (lambda* (#:key outputs #:allow-other-keys)
323
             (for-each
324
               (lambda (file)
325
                 (install-file
326
                   file
327
                   (string-append
328
                     (assoc-ref outputs "out")
329
                     "/lib/coq/user-contrib/compcert/" (dirname file))))
330
               (find-files "." ".*.vo$"))
331
             #t)))
332
       #:tests? #f))
333
    (native-inputs
334
     `(("ocaml" ,ocaml)
335
       ("coq" ,coq-8.7)))
336
    (inputs
337
     `(("menhir" ,ocaml-menhir)))
338
    (home-page "http://compcert.inria.fr")
339
    (synopsis "Certified C compiler")
340
    (description "CompCert is a certified (with coq) C compiler.  Warning: this
341
package is not free software!")
342
    ;; actually the "INRIA Non-Commercial License Agreement"
343
    ;; a non-free license.
344
    (license (license:non-copyleft "file:///LICENSE"))))
345
346
(define-public ocaml-c2newspeak
347
  (package
348
    (name "ocaml-c2newspeak")
349
    (version "1")
350
    (source (origin
351
              (method git-fetch)
352
              (uri (git-reference
353
                     (url "https://github.com/airbus-seclab/c2newspeak")
354
                     (commit "c97fd380111a49fa7baeb9e49c45238fca627492")))
355
              (file-name (string-append name "-" version))
356
              (sha256
357
               (base32
358
                "0fxh868s5jraq61mnig9ilhyjzsq4iw32f20zh3982naanp4p8r6"))))
359
    (build-system ocaml-build-system)
360
    (arguments
361
     `(#:test-target "check"
362
       #:tests? #f
363
       #:phases
364
       (modify-phases %standard-phases
365
         (delete 'configure)
366
         (add-after 'install 'install-bin
367
           (lambda* (#:key outputs #:allow-other-keys)
368
             (install-file "bin/c2newspeak" (string-append (assoc-ref outputs "out") "/bin")))))))
369
    (home-page "https://github.com/airbus-seclab/c2newspeak")
370
    (synopsis "")
371
    (description "")
372
    (license license:lgpl2.1+)))
373
374
(define-public ocaml-bincat
375
  (package
376
    (name "ocaml-bincat")
377
    (version "0.8.1")
378
    (source (origin
379
              (method url-fetch)
380
              (uri (string-append "https://github.com/airbus-seclab/bincat/archive/v"
381
                                  version ".tar.gz"))
382
              (file-name (string-append name "-" version ".tar.gz"))
383
              (sha256
384
               (base32
385
                "1ncwm1h428x1bs4sq7ql1isrkhw0angglsa9hnsvhhw2i1jsdk7j"))))
386
    (build-system ocaml-build-system)
387
    (arguments
388
     `(#:tests? #f; disabled for now
389
       #:validate-runpath? #f; disabled for now
390
       #:make-flags
391
       (list (string-append "PREFIX=" (assoc-ref %outputs "out"))
392
             "LDCONFIG=true"
393
             (string-append "CFLAGS+=-I " (assoc-ref %build-inputs "ocaml")
394
                            "/lib/ocaml"))
395
       #:phases
396
       (modify-phases %standard-phases
397
         (delete 'configure)
398
         (add-before 'build 'python-path
399
           (lambda* (#:key outputs #:allow-other-keys)
400
             (setenv "PYTHONPATH" (string-append (getenv "PYTHONPATH")
401
                                                 ":../python:"
402
                                                 (assoc-ref outputs "out")
403
                                                 "/lib/python2.7/site-packages/"))
404
             #t))
405
         (add-before 'build 'fix-makefiles
406
           (lambda _
407
             (substitute* "ocaml/src/Makefile"
408
               (("GITVERSION:=.*") "GITVERSION:=0.8.1\n"))
409
             (substitute* "python/Makefile"
410
               (("./setup.py install") "./setup.py install --prefix=$(PREFIX)"))
411
             #t))
412
         (add-before 'check 'fix-test
413
           (lambda _
414
             (setenv "PATH" (string-append (getenv "PATH") ":" (getcwd) "/ocaml/src"))
415
             ;; Remove tests that require an armv8 compiler
416
             (substitute* "test/Makefile"
417
               (("eggloader_armv8 eggloader_armv7 eggloader_armv7thumb") ""))
418
             (chmod "test/eggloader_x86" #o755)
419
             #t))
420
         (add-before 'install 'install-python-dir
421
           (lambda* (#:key outputs #:allow-other-keys)
422
             (mkdir-p (string-append (assoc-ref outputs "out")
423
                                     "/lib/python2.7/site-packages/")))))))
424
    (inputs
425
     `(("c2newspeak" ,ocaml-c2newspeak)
426
       ("zarith" ,ocaml-zarith)
427
       ("menhir" ,ocaml-menhir)
428
       ("ocamlgraph" ,ocaml-graph)
429
       ("ocaml-cppo" ,ocaml-cppo)
430
       ("ocaml-ppx-tools" ,ocaml-ppx-tools)
431
       ("gmp" ,gmp)))
432
    (native-inputs
433
     `(("python" ,python-2)
434
       ("pytest" ,python2-pytest)
435
       ("sphinx" ,python2-sphinx)
436
       ("nasm" ,nasm)))
437
    (home-page "https://github.com/airbus-seclab/bincat")
438
    (synopsis "")
439
    (description "")
440
    (license license:lgpl2.1+)))
441
442
(define-public ocaml-ocplib-simplex
443
  (package
444
    (name "ocaml-ocplib-simplex")
445
    (version "0.4")
446
    (source (origin
447
              (method url-fetch)
448
              (uri (string-append "https://github.com/OCamlPro-Iguernlala/"
449
                                  "ocplib-simplex/archive/v" version ".tar.gz"))
450
              (sha256
451
               (base32
452
                "0y6q4bgly7fisdklriww48aknqf2vg4dphr7wwnd1wh80l4anzg1"))))
453
    (build-system gnu-build-system)
454
    (arguments
455
     `(#:tests? #f; Compilation error
456
       #:phases
457
       (modify-phases %standard-phases
458
         (add-after 'unpack 'autoreconf
459
           (lambda _
460
             (invoke "autoreconf" "-fiv")
461
             #t))
462
         (add-before 'install 'mkdir
463
           (lambda* (#:key outputs #:allow-other-keys)
464
             (let* ((out (assoc-ref outputs "out"))
465
                    (lib (string-append out "/lib")))
466
               (mkdir-p lib)
467
               #t))))))
468
    (native-inputs
469
     `(("autoconf" ,autoconf)
470
       ("automake" ,automake)
471
       ("ocaml" ,ocaml)
472
       ("ocaml-findlib" ,ocaml-findlib)
473
       ("which" ,which)))
474
    (home-page "")
475
    (synopsis "")
476
    (description "")
477
    ; lgpl2.1+ with linking exception
478
    (license license:lgpl2.1+)))
479
480
(define-public frama-c
481
  (package
482
    (name "frama-c")
483
    (version "20171101")
484
    (source (origin
485
              (method url-fetch)
486
              (uri (string-append "http://frama-c.com/download/frama-c-Sulfur-"
487
                                  version ".tar.gz"))
488
              (sha256
489
               (base32
490
                "1vwjfqmm1r36gkybsy3a7m89q5zicf4rnz5vlsn9imnpjpl9gjw1"))))
491
    (build-system ocaml-build-system)
492
    (arguments
493
     `(#:tests? #f; for now
494
       #:phases
495
       (modify-phases %standard-phases
496
         (add-before 'configure 'export-shell
497
           (lambda* (#:key inputs #:allow-other-keys)
498
             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
499
                                                   "/bin/sh")))))))
500
    (inputs
501
     `(("gmp" ,gmp)
502
       ("ocaml-graph" ,ocaml-graph)
503
       ("ocaml-zarith" ,ocaml-zarith)))
504
    (home-page "")
505
    (synopsis "")
506
    (description "")
507
    (license license:lgpl2.1+)))
508