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 ocaml-4.07 |
56 | (package |
57 | (inherit ocaml) |
58 | (version "4.07.0") |
59 | (source (origin |
60 | (method url-fetch) |
61 | (uri (string-append |
62 | "http://caml.inria.fr/pub/distrib/ocaml-" |
63 | (version-major+minor version) |
64 | "/ocaml-" version ".tar.xz")) |
65 | (sha256 |
66 | (base32 |
67 | "03wzkzv6w4rdiiva20g5amz0n4x75swpjl8d80468p6zm8hgfnzl")))) |
68 | (arguments |
69 | `(#:phases |
70 | (modify-phases %standard-phases |
71 | (add-after 'unpack 'patch-/bin/sh-references |
72 | (lambda* (#:key inputs #:allow-other-keys) |
73 | (let* ((sh (string-append (assoc-ref inputs "bash") |
74 | "/bin/sh")) |
75 | (quoted-sh (string-append "\"" sh "\""))) |
76 | (with-fluids ((%default-port-encoding #f)) |
77 | (for-each |
78 | (lambda (file) |
79 | (substitute* file |
80 | (("\"/bin/sh\"") |
81 | (begin |
82 | (format (current-error-port) "\ |
83 | patch-/bin/sh-references: ~a: changing `\"/bin/sh\"' to `~a'~%" |
84 | file quoted-sh) |
85 | quoted-sh)))) |
86 | (find-files "." "\\.ml$")) |
87 | #t)))) |
88 | (replace 'configure |
89 | (lambda* (#:key outputs #:allow-other-keys) |
90 | (let* ((out (assoc-ref outputs "out")) |
91 | (mandir (string-append out "/share/man"))) |
92 | ;; Custom configure script doesn't recognize |
93 | ;; --prefix=<PREFIX> syntax (with equals sign). |
94 | (invoke "./configure" |
95 | "--prefix" out |
96 | "--mandir" mandir)) |
97 | #t)) |
98 | (replace 'build |
99 | (lambda _ |
100 | (invoke "make" "-j" (number->string |
101 | (parallel-job-count)) |
102 | "world.opt") |
103 | #t)) |
104 | (delete 'check) |
105 | (add-after 'install 'check |
106 | (lambda _ |
107 | (with-directory-excursion "testsuite" |
108 | (invoke "make" "all")) |
109 | #t))))))) |
110 | |
111 | (define-public ocaml-fix |
112 | (package |
113 | (inherit ocaml) |
114 | (version "4.06.0") |
115 | (source (origin |
116 | (method url-fetch) |
117 | (uri (string-append |
118 | "http://caml.inria.fr/pub/distrib/ocaml-" |
119 | (version-major+minor version) |
120 | "/ocaml-" version ".tar.xz")) |
121 | (sha256 |
122 | (base32 |
123 | "1dy542yfnnw10zvh5s9qzswliq11mg7l0bcyss3501qw3vwvadhj")))) |
124 | (arguments |
125 | `(#:modules ((guix build gnu-build-system) |
126 | (guix build utils) |
127 | (web server)) |
128 | #:phases |
129 | (modify-phases %standard-phases |
130 | (add-after 'unpack 'patch-/bin/sh-references |
131 | (lambda* (#:key inputs #:allow-other-keys) |
132 | (let* ((sh (string-append (assoc-ref inputs "bash") |
133 | "/bin/sh")) |
134 | (quoted-sh (string-append "\"" sh "\""))) |
135 | (with-fluids ((%default-port-encoding #f)) |
136 | (for-each |
137 | (lambda (file) |
138 | (substitute* file |
139 | (("\"/bin/sh\"") |
140 | (begin |
141 | (format (current-error-port) "\ |
142 | patch-/bin/sh-references: ~a: changing `\"/bin/sh\"' to `~a'~%" |
143 | file quoted-sh) |
144 | quoted-sh)))) |
145 | (find-files "." "\\.ml$")) |
146 | #t)))) |
147 | (replace 'configure |
148 | (lambda* (#:key outputs #:allow-other-keys) |
149 | (let* ((out (assoc-ref outputs "out")) |
150 | (mandir (string-append out "/share/man"))) |
151 | ;; Custom configure script doesn't recognize |
152 | ;; --prefix=<PREFIX> syntax (with equals sign). |
153 | (invoke "./configure" |
154 | "--prefix" out |
155 | "--mandir" mandir)) |
156 | #t)) |
157 | (replace 'build |
158 | (lambda _ |
159 | (invoke "make" "-j1" ;; fails to build otherwise |
160 | "world.opt") |
161 | #t)) |
162 | (delete 'check) |
163 | (add-after 'install 'check |
164 | (lambda _ |
165 | (with-directory-excursion "testsuite" |
166 | (invoke "make" "all")) |
167 | #t))))))) |
168 | |
169 | (define-public proof-general2 |
170 | (package |
171 | (name "proof-general2") |
172 | (version "4.4") |
173 | (source (origin |
174 | (method url-fetch) |
175 | (uri (string-append |
176 | "https://github.com/ProofGeneral/PG/archive/v" |
177 | version ".tar.gz")) |
178 | (file-name (string-append name "-" version ".tar.gz")) |
179 | (sha256 |
180 | (base32 |
181 | "0zif2fv6mm4pv75nh10q3p37n293495rvx470bx7ma382zc3d8hv")))) |
182 | (build-system gnu-build-system) |
183 | (native-inputs |
184 | `(("which" ,which) |
185 | ("emacs" ,emacs-minimal) |
186 | ("texinfo" ,texinfo))) |
187 | (inputs |
188 | `(("host-emacs" ,emacs) |
189 | ("perl" ,perl) |
190 | ("coq" ,coq))) |
191 | (arguments |
192 | `(#:tests? #f ; no check target |
193 | #:make-flags (list (string-append "PREFIX=" %output) |
194 | (string-append "DEST_PREFIX=" %output) |
195 | "-j1") |
196 | #:modules ((guix build gnu-build-system) |
197 | (guix build utils) |
198 | (guix build emacs-utils)) |
199 | #:imported-modules (,@%gnu-build-system-modules |
200 | (guix build emacs-utils)) |
201 | #:phases |
202 | (modify-phases %standard-phases |
203 | (delete 'configure) |
204 | (add-after 'unpack 'disable-byte-compile-error-on-warn |
205 | (lambda _ |
206 | (substitute* "Makefile" |
207 | (("\\(setq byte-compile-error-on-warn t\\)") |
208 | "(setq byte-compile-error-on-warn nil)")) |
209 | #t)) |
210 | (add-after 'unpack 'patch-hardcoded-paths |
211 | (lambda* (#:key inputs outputs #:allow-other-keys) |
212 | (let ((out (assoc-ref outputs "out")) |
213 | (coq (assoc-ref inputs "coq")) |
214 | (emacs (assoc-ref inputs "host-emacs"))) |
215 | (define (coq-prog name) |
216 | (string-append coq "/bin/" name)) |
217 | (substitute* "pgshell/pgshell.el" |
218 | (("/bin/sh") (which "sh"))) |
219 | ;(emacs-substitute-variables "coq/coq.el" |
220 | ; ("coq-prog-name" (coq-prog "coqtop")) |
221 | ; ("coq-compiler" (coq-prog "coqc")) |
222 | ; ("coq-dependency-analyzer" (coq-prog "coqdep"))) |
223 | (substitute* "Makefile" |
224 | (("/sbin/install-info") "install-info")) |
225 | (substitute* "bin/proofgeneral" |
226 | (("^PGHOMEDEFAULT=.*" all) |
227 | (string-append all |
228 | "PGHOME=$PGHOMEDEFAULT\n" |
229 | "EMACS=" emacs "/bin/emacs"))) |
230 | #t)))))) |
231 | ;(add-after 'unpack 'clean |
232 | ; (lambda _ |
233 | ; ;; Delete the pre-compiled elc files for Emacs 23. |
234 | ; (zero? (system* "make" "clean")))) |
235 | ;(add-after 'install 'install-doc |
236 | ; (lambda* (#:key make-flags #:allow-other-keys) |
237 | ; ;; XXX FIXME avoid building/installing pdf files, |
238 | ; ;; due to unresolved errors building them. |
239 | ; (substitute* "Makefile" |
240 | ; ((" [^ ]*\\.pdf") "")) |
241 | ; (zero? (apply system* "make" "install-doc" |
242 | ; make-flags))))))) |
243 | (home-page "http://proofgeneral.inf.ed.ac.uk/") |
244 | (synopsis "Generic front-end for proof assistants based on Emacs") |
245 | (description |
246 | "Proof General is a major mode to turn Emacs into an interactive proof |
247 | assistant to write formal mathematical proofs using a variety of theorem |
248 | provers.") |
249 | (license license:gpl2+))) |
250 | |
251 | (define-public ocaml-build |
252 | (package |
253 | (name "ocaml-build") |
254 | (version "0.11.0") |
255 | (source (origin |
256 | (method url-fetch) |
257 | (uri (string-append "https://github.com/ocaml/ocamlbuild/archive/" |
258 | version ".tar.gz")) |
259 | (file-name (string-append name "-" version ".tar.gz")) |
260 | (sha256 |
261 | (base32 |
262 | "1vh30731gv1brr4ljfzd6m5lni44ifyb1w8hwir81ff9874fs5qp")))) |
263 | (build-system gnu-build-system) |
264 | (arguments |
265 | `(#:test-target "test" |
266 | #:tests? #f; FIXME: tests fail to find Findlib |
267 | #:make-flags |
268 | (list (string-append "OCAMLBUILD_PREFIX=" (assoc-ref %outputs "out")) |
269 | (string-append "OCAMLBUILD_BINDIR=" (assoc-ref %outputs "out") "/bin") |
270 | (string-append "OCAMLBUILD_LIBDIR=" (assoc-ref %outputs "out") "/lib") |
271 | (string-append "OCAMLBUILD_MANDIR=" (assoc-ref %outputs "out") "/share/man")) |
272 | #:phases |
273 | (modify-phases %standard-phases |
274 | (delete 'bootstrap) |
275 | (delete 'configure) |
276 | ;(replace 'configure |
277 | ; (lambda* (#:key outputs #:allow-other-keys) |
278 | ; (let ((out (assoc-ref %outputs "out"))) |
279 | ; (zero? (system* "make" "-f" "configure.make" "all"))))) |
280 | (add-before 'build 'findlib-environment |
281 | (lambda* (#:key outputs #:allow-other-keys) |
282 | (let* ((out (assoc-ref outputs "out"))) |
283 | (setenv "OCAMLFIND_DESTDIR" (string-append out "/lib/ocaml/site-lib")) |
284 | (setenv "OCAMLFIND_LDCONF" "ignore") |
285 | #t)))))) |
286 | (native-inputs |
287 | `(("ocaml" ,ocaml-fix))) |
288 | (home-page "") |
289 | (synopsis "") |
290 | (description "") |
291 | (license license:lgpl2.1+))) |
292 | |
293 | (define-public camlp4-fix |
294 | (package |
295 | (inherit camlp4) |
296 | (name "camlp4") |
297 | (version "4.06+1") |
298 | (source (origin |
299 | (method url-fetch) |
300 | (uri (string-append "https://github.com/ocaml/camlp4/archive/" |
301 | version ".tar.gz")) |
302 | (file-name (string-append name "-" version ".tar.gz")) |
303 | (sha256 |
304 | (base32 |
305 | "08mrp8jjaayv0s50kmhjkafxqykff5dq3073hrl7ylx0km253k5i")))) |
306 | (inputs `(("ocaml" ,ocaml-fix))) |
307 | (native-inputs |
308 | `(("ocaml" ,ocaml-fix) |
309 | ("which" ,which) |
310 | ("build" ,ocaml-build))))) |
311 | |
312 | (define-public ocaml-findlib-fix |
313 | (package |
314 | (inherit ocaml-findlib) |
315 | (version "1.7.3") |
316 | (source (origin |
317 | (method url-fetch) |
318 | (uri (string-append "http://download.camlcity.org/download/findlib-" |
319 | version ".tar.gz")) |
320 | (sha256 |
321 | (base32 |
322 | "12xx8si1qv3xz90qsrpazjjk4lc1989fzm97rsmc4diwla7n15ni")))) |
323 | (arguments |
324 | (substitute-keyword-arguments (package-arguments ocaml-findlib) |
325 | ((#:phases phases) |
326 | `(modify-phases ,phases |
327 | (add-before 'build 'fix-findlib-makefile |
328 | (lambda* (#:key outputs #:allow-other-keys) |
329 | (substitute* "src/findlib/Makefile" |
330 | (("\\$\\(prefix\\)\\$\\(OCAML_CORE_STDLIB\\)") |
331 | (string-append (assoc-ref outputs "out") "/lib/ocaml/site-lib"))) |
332 | #t)))))) |
333 | (native-inputs |
334 | `(("camlp4" ,camlp4-fix) |
335 | ("ocaml" ,ocaml-fix) |
336 | ("m4" ,m4))))) |
337 | |
338 | (define-public camlp5-fix |
339 | (package |
340 | (inherit camlp5) |
341 | (name "camlp5") |
342 | (version "7.03") |
343 | (source (origin |
344 | (method url-fetch) |
345 | (uri (string-append "https://github.com/camlp5/camlp5/archive/rel" |
346 | (string-delete #\. version) ".tar.gz")) |
347 | (sha256 |
348 | (base32 |
349 | "06pj7l75r586gngam7nspd1a13ay7cj2bjh035z64w4fgaahlgf1")))) |
350 | (inputs |
351 | `(("ocaml" ,ocaml-fix))))) |
352 | |
353 | (define-public lablgtk-fix |
354 | (package |
355 | (inherit lablgtk) |
356 | (version "2.18.6") |
357 | (source (origin |
358 | (method url-fetch) |
359 | (uri (ocaml-forge-uri "lablgtk" version 1726)) |
360 | (sha256 |
361 | (base32 |
362 | "1y38fdvswy6hmppm65qvgdk4pb3ghhnvz7n4ialf46340r1s5p2d")))) |
363 | (arguments |
364 | `(#:tests? #f ; no check target |
365 | |
366 | ;; opt: also install cmxa files |
367 | #:make-flags (list "all" "opt" |
368 | "OCAMLFIND=ocamlfind" |
369 | "OCAMLLDCONF=ld.conf" |
370 | (string-append "FINDLIBDIR=" |
371 | (assoc-ref %outputs "out") |
372 | "/lib/ocaml")) |
373 | ;; Occasionally we would get "Error: Unbound module GtkThread" when |
374 | ;; compiling 'gtkThInit.ml', with 'make -j'. So build sequentially. |
375 | #:parallel-build? #f |
376 | |
377 | #:phases |
378 | (modify-phases %standard-phases |
379 | (add-before 'install 'prepare-install |
380 | (lambda* (#:key inputs outputs #:allow-other-keys) |
381 | (let ((out (assoc-ref outputs "out")) |
382 | (ocaml (assoc-ref inputs "ocaml"))) |
383 | ;; Install into the output and not the ocaml directory. |
384 | (mkdir-p (string-append out "/lib/ocaml")) |
385 | (substitute* "config.make" |
386 | ((ocaml) out)) |
387 | #t)))))) |
388 | (home-page "http://lablgtk.forge.ocamlcore.org/") |
389 | (native-inputs |
390 | `(("ocaml" ,ocaml-fix) |
391 | ("build" ,ocaml-build) |
392 | ("camlp4" ,camlp4-fix) |
393 | ("findlib" ,ocaml-findlib-fix) |
394 | ("pkg-config" ,pkg-config))))) |
395 | |
396 | (define-public ocaml-menhir-fix |
397 | (package |
398 | (inherit ocaml-menhir) |
399 | (version "20170607") |
400 | (name "ocaml-menhir-fix") |
401 | (source (origin |
402 | (method url-fetch) |
403 | (uri (string-append |
404 | "http://gallium.inria.fr/~fpottier/menhir/" |
405 | "menhir-" version ".tar.gz")) |
406 | (sha256 |
407 | (base32 |
408 | "0qffci9qxgfabzyalx851q994yykl4n9ylr4vbplsm6is1padjh0")))) |
409 | (inputs |
410 | `(("ocaml" ,ocaml-fix) |
411 | ("ocamlbuild" ,ocaml-build))))) |
412 | |
413 | (define-public ocaml-num |
414 | (package |
415 | (name "ocaml-num") |
416 | (version "1.1") |
417 | (source (origin |
418 | (method url-fetch) |
419 | (uri (string-append "https://github.com/ocaml/num/archive/v" |
420 | version ".tar.gz")) |
421 | (file-name (string-append name "-" version ".tar.gz")) |
422 | (sha256 |
423 | (base32 |
424 | "1xlkd0svc0mgq5s7nrm2rjrsvg15i9wxqkc1kvwjp6sv8vv8bb04")))) |
425 | (build-system ocaml-build-system) |
426 | (arguments |
427 | `(#:ocaml ,ocaml-fix |
428 | #:findlib ,ocaml-findlib-fix |
429 | #:phases |
430 | (modify-phases %standard-phases |
431 | (delete 'configure) |
432 | (add-before 'build 'fix-makefile |
433 | (lambda* (#:key outputs #:allow-other-keys) |
434 | ;; This package supposes we install to the same directory as |
435 | ;; the ocaml package. |
436 | (substitute* "src/META" |
437 | (("\"\\^\"") (string-append "\"" (assoc-ref outputs "out") |
438 | "/lib/ocaml/site-lib\""))) |
439 | (substitute* "src/Makefile" |
440 | (("\\) \\$\\(STDLIBDIR\\)") |
441 | (string-append ") " (assoc-ref outputs "out") |
442 | "/lib/ocaml/site-lib"))) |
443 | #t))))) |
444 | (home-page "https://github.com/ocaml/num") |
445 | (synopsis "Arbitrary-precision integer and rational arithmetic") |
446 | (description "OCaml-Num contains the legacy Num library for |
447 | arbitrary-precision integer and rational arithmetic that used to be part of |
448 | the OCaml core distribution.") |
449 | (license license:lgpl2.1+))); with linking exception |
450 | |
451 | (define-public coq-8.7 |
452 | (package |
453 | (inherit coq) |
454 | (name "coq") |
455 | (version "8.7.2") |
456 | (source (origin |
457 | (method url-fetch) |
458 | (uri (string-append "https://github.com/coq/coq/archive/V" |
459 | version ".tar.gz")) |
460 | (file-name (string-append name "-" version ".tar.gz")) |
461 | (sha256 |
462 | (base32 |
463 | "1lkqvs7ayzv5kkg26y837pg0d6r2b5hbjxl71ba93f39kybw69gg")))) |
464 | (native-inputs |
465 | `(("ocamlbuild" ,ocaml-build) |
466 | ("hevea" ,hevea) |
467 | ("texlive" ,texlive))) |
468 | (inputs |
469 | `(("lablgtk" ,lablgtk-fix) |
470 | ("python" ,python-2) |
471 | ("camlp5" ,camlp5-fix) |
472 | ;; ocaml-num was removed from the ocaml package in 4.06. |
473 | ("ocaml-num" ,ocaml-num))) |
474 | (arguments |
475 | `(#:ocaml ,ocaml-fix |
476 | #:findlib ,ocaml-findlib-fix |
477 | #:phases |
478 | (modify-phases %standard-phases |
479 | (replace 'configure |
480 | (lambda* (#:key outputs #:allow-other-keys) |
481 | (let* ((out (assoc-ref outputs "out")) |
482 | (mandir (string-append out "/share/man")) |
483 | (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) |
484 | (invoke "./configure" |
485 | "-prefix" out |
486 | "-mandir" mandir |
487 | "-browser" browser |
488 | "-coqide" "opt")) |
489 | #t)) |
490 | (replace 'build |
491 | (lambda* (#:key inputs #:allow-other-keys) |
492 | (substitute* "ide/ideutils.ml" |
493 | (("Bytes.unsafe_to_string read_string") "read_string")) |
494 | (invoke "make" "-j" (number->string |
495 | (parallel-job-count)) |
496 | (string-append |
497 | "USERFLAGS=-I " |
498 | (assoc-ref inputs "ocaml-num") |
499 | "/lib/ocaml/site-lib") |
500 | "world") |
501 | #t)) |
502 | (delete 'check) |
503 | (add-after 'install 'check |
504 | (lambda _ |
505 | (with-directory-excursion "test-suite" |
506 | ;; These two tests fail. |
507 | ;; This one fails because the output is not formatted as expected. |
508 | (delete-file-recursively "coq-makefile/timing") |
509 | ;; This one fails because we didn't build coqtop.byte. |
510 | (delete-file-recursively "coq-makefile/findlib-package") |
511 | (invoke "make")) |
512 | #t))))))) |
513 | |
514 | (define-public coq-fix |
515 | (package |
516 | (inherit coq) |
517 | (native-inputs |
518 | `(("ocamlbuild" ,ocaml-build) |
519 | ("hevea" ,hevea) |
520 | ("texlive" ,texlive))) |
521 | (inputs |
522 | `(("lablgtk" ,lablgtk-fix) |
523 | ("python" ,python-2) |
524 | ("camlp5" ,camlp5-fix) |
525 | ;; ocaml-num was removed from the ocaml package in 4.06. |
526 | ("ocaml-num" ,ocaml-num))) |
527 | (arguments |
528 | `(#:ocaml ,ocaml-fix |
529 | #:findlib ,ocaml-findlib-fix |
530 | #:phases |
531 | (modify-phases %standard-phases |
532 | (replace 'configure |
533 | (lambda* (#:key outputs #:allow-other-keys) |
534 | (let* ((out (assoc-ref outputs "out")) |
535 | (mandir (string-append out "/share/man")) |
536 | (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) |
537 | (invoke "./configure" |
538 | "-prefix" out |
539 | "-mandir" mandir |
540 | "-browser" browser |
541 | "-coqide" "opt")) |
542 | #t)) |
543 | (replace 'build |
544 | (lambda* (#:key inputs #:allow-other-keys) |
545 | (substitute* "ide/ideutils.ml" |
546 | (("Bytes.unsafe_to_string read_string") "read_string")) |
547 | (invoke "make" "-j" (number->string |
548 | (parallel-job-count)) |
549 | (string-append |
550 | "USERFLAGS=-I " |
551 | (assoc-ref inputs "ocaml-num") |
552 | "/lib/ocaml/site-lib") |
553 | "world") |
554 | #t)) |
555 | (delete 'check) |
556 | (add-after 'install 'check |
557 | (lambda _ |
558 | (with-directory-excursion "test-suite" |
559 | ;; These two tests fail. |
560 | ;; This one fails because the output is not formatted as expected. |
561 | (delete-file-recursively "coq-makefile/timing") |
562 | ;; This one fails because we didn't build coqtop.byte. |
563 | (delete-file-recursively "coq-makefile/findlib-package") |
564 | (invoke "make")) |
565 | #t))))))) |
566 | |
567 | (define-public coq-bignums-8.7 |
568 | (package |
569 | (inherit coq-bignums) |
570 | (name "coq-bignums") |
571 | (version "8.7.0") |
572 | (source (origin |
573 | (method url-fetch) |
574 | (uri (string-append "https://github.com/coq/bignums/archive/V" |
575 | version ".tar.gz")) |
576 | (file-name (string-append name "-" version ".tar.gz")) |
577 | (sha256 |
578 | (base32 |
579 | "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx")))) |
580 | (native-inputs |
581 | `(("ocaml-fix" ,ocaml-fix) |
582 | ("coq-8.7" ,coq-8.7))) |
583 | (inputs |
584 | `(("camlp5-fix" ,camlp5-fix))))) |
585 | |
586 | (define-public ppsimpl |
587 | (package |
588 | (name "ppsimpl") |
589 | (version "8.7") |
590 | (source (origin |
591 | (method git-fetch) |
592 | (uri (git-reference |
593 | (url "https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git") |
594 | (commit "86255a47568df58767d1d8e0b9e2da31cf73a5fc"))) |
595 | (file-name (string-append name "-" version)) |
596 | (sha256 |
597 | (base32 |
598 | "0h509w43j2wd2pyx04k3xfd0bsbmqscwqvhf8whzc3cxzl4j6vvq")))) |
599 | ;(uri "https://gforge.inria.fr/frs/download.php/file/37615/ppsimpl-09-07-2018.tar.gz") |
600 | ;(sha256 |
601 | ; (base32 |
602 | ; "010zgskc1wd5v6wmmyxaapvwxjlgbdqqiks2dvf6llx03b07ak59")))) |
603 | (build-system gnu-build-system) |
604 | (arguments |
605 | `(#:test-target "test" |
606 | #:configure-flags |
607 | (list "-R" (string-append (assoc-ref %build-inputs "compcert") "/lib/coq/user-contrib/compcert") "compcert") |
608 | #:make-flags (list "COQC=coqc -R src PP -I src" |
609 | (string-append |
610 | "COQLIBINSTALL=" |
611 | (assoc-ref %outputs "out") |
612 | "/lib/coq/user-contrib")))) |
613 | (inputs |
614 | `(("coq-bignums-8.7" ,coq-bignums-8.7) |
615 | ("compcert" ,compcert))) |
616 | (native-inputs |
617 | `(("coq-8.7" ,coq-8.7) |
618 | ("ocaml-fix" ,ocaml-fix) |
619 | ("ocaml-findlib-fix" ,ocaml-findlib-fix) |
620 | ("camlp4-fix" ,camlp4-fix) |
621 | ("camlp5-fix" ,camlp5-fix) |
622 | ("which" ,which))) |
623 | (home-page "") |
624 | (synopsis "") |
625 | (description "") |
626 | ;; No declared license -> all rights reserved |
627 | (license #f))) |
628 | |
629 | (define-public compcert |
630 | (package |
631 | (name "compcert") |
632 | (version "3.3") |
633 | (source (origin |
634 | (method url-fetch) |
635 | (uri (string-append "http://compcert.inria.fr/release/compcert-" |
636 | version ".tgz")) |
637 | (sha256 |
638 | (base32 |
639 | "16xrqcwak1v1fk5ndx6jf1yvxv3adsr7p7z34gfm2mpggxnq0xwn")))) |
640 | (build-system gnu-build-system) |
641 | (arguments |
642 | `(#:phases |
643 | (modify-phases %standard-phases |
644 | (replace 'configure |
645 | (lambda* (#:key outputs #:allow-other-keys) |
646 | (let ((system ,(match (or (%current-target-system) (%current-system)) |
647 | ("x86_64-linux" "x86_64-linux") |
648 | ("i686-linux" "x86_32-linux") |
649 | ("armhf-linux" "arm-linux")))) |
650 | (format #t "Building for ~a~%" system) |
651 | (invoke "./configure" system "-prefix" |
652 | (assoc-ref outputs "out"))) |
653 | #t)) |
654 | (add-after 'install 'install-lib |
655 | (lambda* (#:key outputs #:allow-other-keys) |
656 | (for-each |
657 | (lambda (file) |
658 | (install-file |
659 | file |
660 | (string-append |
661 | (assoc-ref outputs "out") |
662 | "/lib/coq/user-contrib/compcert/" (dirname file)))) |
663 | (find-files "." ".*.vo$")) |
664 | #t))) |
665 | #:tests? #f)) |
666 | (native-inputs |
667 | `(("ocaml" ,ocaml-fix) |
668 | ("coq" ,coq-8.7))) |
669 | (inputs |
670 | `(("menhir" ,ocaml-menhir-fix))) |
671 | (home-page "http://compcert.inria.fr") |
672 | (synopsis "Certified C compiler") |
673 | (description "CompCert is a certified (with coq) C compiler. Warning: this |
674 | package is not free software!") |
675 | ;; actually the "INRIA Non-Commercial License Agreement" |
676 | ;; a non-free license. |
677 | (license (license:non-copyleft "file:///LICENSE")))) |
678 | |
679 | (define-public cubicle |
680 | (package |
681 | (name "cubicle") |
682 | (version "1.1.1") |
683 | (source (origin |
684 | (method url-fetch) |
685 | (uri (string-append "http://cubicle.lri.fr/cubicle-" |
686 | version ".tar.gz")) |
687 | (sha256 |
688 | (base32 |
689 | "1sny9c4fm14k014pk62ibpwbrjjirkx8xmhs9jg7q1hk7y7x3q2h")))) |
690 | (build-system gnu-build-system) |
691 | (native-inputs |
692 | `(("ocaml" ,ocaml) |
693 | ("which" ,which))) |
694 | (propagated-inputs |
695 | `(("z3" ,z3))) |
696 | (arguments |
697 | `(#:configure-flags (list "--with-z3") |
698 | #:tests? #f |
699 | #:phases |
700 | (modify-phases %standard-phases |
701 | (add-before 'configure 'configure-for-release |
702 | (lambda _ |
703 | (substitute* "Makefile.in" |
704 | (("SVNREV=") "#SVNREV=")))) |
705 | (add-before 'configure 'fix-/bin/sh |
706 | (lambda _ |
707 | (substitute* "configure" |
708 | (("/bin/sh") (which "sh"))))) |
709 | (add-before 'configure 'fix-smt-z3wrapper.ml |
710 | (lambda _ |
711 | (substitute* "Makefile.in" |
712 | (("\\\\n") ""))))))) |
713 | (home-page "http://cubicle.lri.fr/") |
714 | (synopsis "Model checker for array-based systems") |
715 | (description "Cubicle is an open source model checker for verifying safety |
716 | properties of array-based systems. This is a syntactically restricted class of |
717 | parametrized transition systems with states represented as arrays indexed by an |
718 | arbitrary number of processes. Cache coherence protocols and mutual exclusion |
719 | algorithms are typical examples of such systems.") |
720 | (license license:asl2.0))) |
721 | |
722 | (define-public ocaml-c2newspeak |
723 | (package |
724 | (name "ocaml-c2newspeak") |
725 | (version "1") |
726 | (source (origin |
727 | (method git-fetch) |
728 | (uri (git-reference |
729 | (url "https://github.com/airbus-seclab/c2newspeak") |
730 | (commit "c97fd380111a49fa7baeb9e49c45238fca627492"))) |
731 | (file-name (string-append name "-" version)) |
732 | (sha256 |
733 | (base32 |
734 | "0fxh868s5jraq61mnig9ilhyjzsq4iw32f20zh3982naanp4p8r6")))) |
735 | (build-system ocaml-build-system) |
736 | (arguments |
737 | `(#:test-target "check" |
738 | #:tests? #f |
739 | #:phases |
740 | (modify-phases %standard-phases |
741 | (delete 'configure) |
742 | (add-after 'install 'install-bin |
743 | (lambda* (#:key outputs #:allow-other-keys) |
744 | (install-file "bin/c2newspeak" (string-append (assoc-ref outputs "out") "/bin"))))))) |
745 | (home-page "https://github.com/airbus-seclab/c2newspeak") |
746 | (synopsis "") |
747 | (description "") |
748 | (license license:lgpl2.1+))) |
749 | |
750 | (define-public ocaml-bincat |
751 | (package |
752 | (name "ocaml-bincat") |
753 | (version "0.8.1") |
754 | (source (origin |
755 | (method url-fetch) |
756 | (uri (string-append "https://github.com/airbus-seclab/bincat/archive/v" |
757 | version ".tar.gz")) |
758 | (file-name (string-append name "-" version ".tar.gz")) |
759 | (sha256 |
760 | (base32 |
761 | "1ncwm1h428x1bs4sq7ql1isrkhw0angglsa9hnsvhhw2i1jsdk7j")))) |
762 | (build-system ocaml-build-system) |
763 | (arguments |
764 | `(#:tests? #f; disabled for now |
765 | #:validate-runpath? #f; disabled for now |
766 | #:make-flags |
767 | (list (string-append "PREFIX=" (assoc-ref %outputs "out")) |
768 | "LDCONFIG=true" |
769 | (string-append "CFLAGS+=-I " (assoc-ref %build-inputs "ocaml") |
770 | "/lib/ocaml")) |
771 | #:phases |
772 | (modify-phases %standard-phases |
773 | (delete 'configure) |
774 | (add-before 'build 'python-path |
775 | (lambda* (#:key outputs #:allow-other-keys) |
776 | (setenv "PYTHONPATH" (string-append (getenv "PYTHONPATH") |
777 | ":../python:" |
778 | (assoc-ref outputs "out") |
779 | "/lib/python2.7/site-packages/")) |
780 | #t)) |
781 | (add-before 'build 'fix-makefiles |
782 | (lambda _ |
783 | (substitute* "ocaml/src/Makefile" |
784 | (("GITVERSION:=.*") "GITVERSION:=0.8.1\n")) |
785 | (substitute* "python/Makefile" |
786 | (("./setup.py install") "./setup.py install --prefix=$(PREFIX)")) |
787 | #t)) |
788 | (add-before 'check 'fix-test |
789 | (lambda _ |
790 | (setenv "PATH" (string-append (getenv "PATH") ":" (getcwd) "/ocaml/src")) |
791 | ;; Remove tests that require an armv8 compiler |
792 | (substitute* "test/Makefile" |
793 | (("eggloader_armv8 eggloader_armv7 eggloader_armv7thumb") "")) |
794 | (chmod "test/eggloader_x86" #o755) |
795 | #t)) |
796 | (add-before 'install 'install-python-dir |
797 | (lambda* (#:key outputs #:allow-other-keys) |
798 | (mkdir-p (string-append (assoc-ref outputs "out") |
799 | "/lib/python2.7/site-packages/"))))))) |
800 | (inputs |
801 | `(("c2newspeak" ,ocaml-c2newspeak) |
802 | ("zarith" ,ocaml-zarith) |
803 | ("menhir" ,ocaml-menhir) |
804 | ("ocamlgraph" ,ocaml-graph) |
805 | ("ocaml-cppo" ,ocaml-cppo) |
806 | ("ocaml-ppx-tools" ,ocaml-ppx-tools) |
807 | ("gmp" ,gmp))) |
808 | (native-inputs |
809 | `(("python" ,python-2) |
810 | ("pytest" ,python2-pytest) |
811 | ("sphinx" ,python2-sphinx) |
812 | ("nasm" ,nasm))) |
813 | (home-page "https://github.com/airbus-seclab/bincat") |
814 | (synopsis "") |
815 | (description "") |
816 | (license license:lgpl2.1+))) |
817 | |
818 | (define-public ocaml-ocplib-simplex |
819 | (package |
820 | (name "ocaml-ocplib-simplex") |
821 | (version "0.4") |
822 | (source (origin |
823 | (method url-fetch) |
824 | (uri (string-append "https://github.com/OCamlPro-Iguernlala/" |
825 | "ocplib-simplex/archive/v" version ".tar.gz")) |
826 | (sha256 |
827 | (base32 |
828 | "0y6q4bgly7fisdklriww48aknqf2vg4dphr7wwnd1wh80l4anzg1")))) |
829 | (build-system gnu-build-system) |
830 | (arguments |
831 | `(#:tests? #f; Compilation error |
832 | #:phases |
833 | (modify-phases %standard-phases |
834 | (add-after 'unpack 'autoreconf |
835 | (lambda _ |
836 | (invoke "autoreconf" "-fiv") |
837 | #t)) |
838 | (add-before 'install 'mkdir |
839 | (lambda* (#:key outputs #:allow-other-keys) |
840 | (let* ((out (assoc-ref outputs "out")) |
841 | (lib (string-append out "/lib"))) |
842 | (mkdir-p lib) |
843 | #t)))))) |
844 | (native-inputs |
845 | `(("autoconf" ,autoconf) |
846 | ("automake" ,automake) |
847 | ("ocaml" ,ocaml) |
848 | ("ocaml-findlib" ,ocaml-findlib) |
849 | ("which" ,which))) |
850 | (home-page "") |
851 | (synopsis "") |
852 | (description "") |
853 | ; lgpl2.1+ with linking exception |
854 | (license license:lgpl2.1+))) |
855 | |
856 | (define-public frama-c |
857 | (package |
858 | (name "frama-c") |
859 | (version "20171101") |
860 | (source (origin |
861 | (method url-fetch) |
862 | (uri (string-append "http://frama-c.com/download/frama-c-Sulfur-" |
863 | version ".tar.gz")) |
864 | (sha256 |
865 | (base32 |
866 | "1vwjfqmm1r36gkybsy3a7m89q5zicf4rnz5vlsn9imnpjpl9gjw1")))) |
867 | (build-system ocaml-build-system) |
868 | (arguments |
869 | `(#:tests? #f; for now |
870 | #:phases |
871 | (modify-phases %standard-phases |
872 | (add-before 'configure 'export-shell |
873 | (lambda* (#:key inputs #:allow-other-keys) |
874 | (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") |
875 | "/bin/sh"))))))) |
876 | (inputs |
877 | `(("gmp" ,gmp) |
878 | ("ocaml-graph" ,ocaml-graph) |
879 | ("ocaml-zarith" ,ocaml-zarith))) |
880 | (home-page "") |
881 | (synopsis "") |
882 | (description "") |
883 | (license license:lgpl2.1+))) |
884 |