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 |