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.6 |
452 | (package |
453 | (inherit coq) |
454 | (name "coq") |
455 | (version "8.6.1") |
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 | "02nm5sn79hrb9fdmkhyclk80jydadf4jcafmr3idwr5h4z56qbms")))) |
464 | ;(native-inputs |
465 | ; `(("ocamlbuild" ,ocaml-build) |
466 | ; ("hevea" ,hevea) |
467 | ; ("texlive" ,texlive))) |
468 | ;(inputs |
469 | ; `(("lablgtk" ,lablgtk) |
470 | ; ("python" ,python-2) |
471 | ; ("camlp5" ,camlp5))) |
472 | (arguments |
473 | `(#:phases |
474 | (modify-phases %standard-phases |
475 | (replace 'configure |
476 | (lambda* (#:key outputs #:allow-other-keys) |
477 | (let* ((out (assoc-ref outputs "out")) |
478 | (mandir (string-append out "/share/man")) |
479 | (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) |
480 | (invoke "./configure" |
481 | "-prefix" out |
482 | "-mandir" mandir |
483 | "-browser" browser |
484 | "-coqide" "opt")) |
485 | #t)) |
486 | (replace 'build |
487 | (lambda* (#:key inputs #:allow-other-keys) |
488 | (substitute* "ide/ideutils.ml" |
489 | (("Bytes.unsafe_to_string read_string") "read_string")) |
490 | (invoke "make" "-j" (number->string |
491 | (parallel-job-count)) |
492 | "world") |
493 | #t)) |
494 | (delete 'check) |
495 | (add-after 'install 'check |
496 | (lambda _ |
497 | (with-directory-excursion "test-suite" |
498 | (invoke "make")) |
499 | #t))))))) |
500 | |
501 | (define-public coq-8.7 |
502 | (package |
503 | (inherit coq) |
504 | (name "coq") |
505 | (version "8.7.2") |
506 | (source (origin |
507 | (method url-fetch) |
508 | (uri (string-append "https://github.com/coq/coq/archive/V" |
509 | version ".tar.gz")) |
510 | (file-name (string-append name "-" version ".tar.gz")) |
511 | (sha256 |
512 | (base32 |
513 | "1lkqvs7ayzv5kkg26y837pg0d6r2b5hbjxl71ba93f39kybw69gg")))) |
514 | (native-inputs |
515 | `(("ocamlbuild" ,ocaml-build) |
516 | ("hevea" ,hevea) |
517 | ("texlive" ,texlive))) |
518 | (inputs |
519 | `(("lablgtk" ,lablgtk-fix) |
520 | ("python" ,python-2) |
521 | ("camlp5" ,camlp5-fix) |
522 | ;; ocaml-num was removed from the ocaml package in 4.06. |
523 | ("ocaml-num" ,ocaml-num))) |
524 | (arguments |
525 | `(#:ocaml ,ocaml-fix |
526 | #:findlib ,ocaml-findlib-fix |
527 | #:phases |
528 | (modify-phases %standard-phases |
529 | (replace 'configure |
530 | (lambda* (#:key outputs #:allow-other-keys) |
531 | (let* ((out (assoc-ref outputs "out")) |
532 | (mandir (string-append out "/share/man")) |
533 | (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) |
534 | (invoke "./configure" |
535 | "-prefix" out |
536 | "-mandir" mandir |
537 | "-browser" browser |
538 | "-coqide" "opt")) |
539 | #t)) |
540 | (replace 'build |
541 | (lambda* (#:key inputs #:allow-other-keys) |
542 | (substitute* "ide/ideutils.ml" |
543 | (("Bytes.unsafe_to_string read_string") "read_string")) |
544 | (invoke "make" "-j" (number->string |
545 | (parallel-job-count)) |
546 | (string-append |
547 | "USERFLAGS=-I " |
548 | (assoc-ref inputs "ocaml-num") |
549 | "/lib/ocaml/site-lib") |
550 | "world") |
551 | #t)) |
552 | (delete 'check) |
553 | (add-after 'install 'check |
554 | (lambda _ |
555 | (with-directory-excursion "test-suite" |
556 | ;; These two tests fail. |
557 | ;; This one fails because the output is not formatted as expected. |
558 | (delete-file-recursively "coq-makefile/timing") |
559 | ;; This one fails because we didn't build coqtop.byte. |
560 | (delete-file-recursively "coq-makefile/findlib-package") |
561 | (invoke "make")) |
562 | #t))))))) |
563 | |
564 | (define-public coq-fix |
565 | (package |
566 | (inherit coq) |
567 | (native-inputs |
568 | `(("ocamlbuild" ,ocaml-build) |
569 | ("hevea" ,hevea) |
570 | ("texlive" ,texlive))) |
571 | (inputs |
572 | `(("lablgtk" ,lablgtk-fix) |
573 | ("python" ,python-2) |
574 | ("camlp5" ,camlp5-fix) |
575 | ;; ocaml-num was removed from the ocaml package in 4.06. |
576 | ("ocaml-num" ,ocaml-num))) |
577 | (arguments |
578 | `(#:ocaml ,ocaml-fix |
579 | #:findlib ,ocaml-findlib-fix |
580 | #:phases |
581 | (modify-phases %standard-phases |
582 | (replace 'configure |
583 | (lambda* (#:key outputs #:allow-other-keys) |
584 | (let* ((out (assoc-ref outputs "out")) |
585 | (mandir (string-append out "/share/man")) |
586 | (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) |
587 | (invoke "./configure" |
588 | "-prefix" out |
589 | "-mandir" mandir |
590 | "-browser" browser |
591 | "-coqide" "opt")) |
592 | #t)) |
593 | (replace 'build |
594 | (lambda* (#:key inputs #:allow-other-keys) |
595 | (substitute* "ide/ideutils.ml" |
596 | (("Bytes.unsafe_to_string read_string") "read_string")) |
597 | (invoke "make" "-j" (number->string |
598 | (parallel-job-count)) |
599 | (string-append |
600 | "USERFLAGS=-I " |
601 | (assoc-ref inputs "ocaml-num") |
602 | "/lib/ocaml/site-lib") |
603 | "world") |
604 | #t)) |
605 | (delete 'check) |
606 | (add-after 'install 'check |
607 | (lambda _ |
608 | (with-directory-excursion "test-suite" |
609 | ;; These two tests fail. |
610 | ;; This one fails because the output is not formatted as expected. |
611 | (delete-file-recursively "coq-makefile/timing") |
612 | ;; This one fails because we didn't build coqtop.byte. |
613 | (delete-file-recursively "coq-makefile/findlib-package") |
614 | (invoke "make")) |
615 | #t))))))) |
616 | |
617 | (define-public coq-bignums-8.7 |
618 | (package |
619 | (inherit coq-bignums) |
620 | (name "coq-bignums") |
621 | (version "8.7.0") |
622 | (source (origin |
623 | (method url-fetch) |
624 | (uri (string-append "https://github.com/coq/bignums/archive/V" |
625 | version ".tar.gz")) |
626 | (file-name (string-append name "-" version ".tar.gz")) |
627 | (sha256 |
628 | (base32 |
629 | "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx")))) |
630 | (native-inputs |
631 | `(("ocaml-fix" ,ocaml-fix) |
632 | ("coq-8.7" ,coq-8.7))) |
633 | (inputs |
634 | `(("camlp5-fix" ,camlp5-fix))))) |
635 | |
636 | (define-public ppsimpl |
637 | (package |
638 | (name "ppsimpl") |
639 | (version "8.7") |
640 | (source (origin |
641 | (method git-fetch) |
642 | (uri (git-reference |
643 | (url "https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git") |
644 | (commit "86255a47568df58767d1d8e0b9e2da31cf73a5fc"))) |
645 | (file-name (string-append name "-" version)) |
646 | (sha256 |
647 | (base32 |
648 | "0h509w43j2wd2pyx04k3xfd0bsbmqscwqvhf8whzc3cxzl4j6vvq")))) |
649 | ;(uri "https://gforge.inria.fr/frs/download.php/file/37615/ppsimpl-09-07-2018.tar.gz") |
650 | ;(sha256 |
651 | ; (base32 |
652 | ; "010zgskc1wd5v6wmmyxaapvwxjlgbdqqiks2dvf6llx03b07ak59")))) |
653 | (build-system gnu-build-system) |
654 | (arguments |
655 | `(#:test-target "test" |
656 | #:configure-flags |
657 | (list "-R" (string-append (assoc-ref %build-inputs "compcert") "/lib/coq/user-contrib/compcert") "compcert") |
658 | #:make-flags (list "COQC=coqc -R src PP -I src" |
659 | (string-append |
660 | "COQLIBINSTALL=" |
661 | (assoc-ref %outputs "out") |
662 | "/lib/coq/user-contrib")))) |
663 | (inputs |
664 | `(("coq-bignums-8.7" ,coq-bignums-8.7) |
665 | ("compcert" ,compcert))) |
666 | (native-inputs |
667 | `(("coq-8.7" ,coq-8.7) |
668 | ("ocaml-fix" ,ocaml-fix) |
669 | ("ocaml-findlib-fix" ,ocaml-findlib-fix) |
670 | ("camlp4-fix" ,camlp4-fix) |
671 | ("camlp5-fix" ,camlp5-fix) |
672 | ("which" ,which))) |
673 | (home-page "") |
674 | (synopsis "") |
675 | (description "") |
676 | ;; No declared license -> all rights reserved |
677 | (license #f))) |
678 | |
679 | (define-public compcert |
680 | (package |
681 | (name "compcert") |
682 | (version "3.3") |
683 | (source (origin |
684 | (method url-fetch) |
685 | (uri (string-append "http://compcert.inria.fr/release/compcert-" |
686 | version ".tgz")) |
687 | (sha256 |
688 | (base32 |
689 | "16xrqcwak1v1fk5ndx6jf1yvxv3adsr7p7z34gfm2mpggxnq0xwn")))) |
690 | (build-system gnu-build-system) |
691 | (arguments |
692 | `(#:phases |
693 | (modify-phases %standard-phases |
694 | (replace 'configure |
695 | (lambda* (#:key outputs #:allow-other-keys) |
696 | (let ((system ,(match (or (%current-target-system) (%current-system)) |
697 | ("x86_64-linux" "x86_64-linux") |
698 | ("i686-linux" "x86_32-linux") |
699 | ("armhf-linux" "arm-linux")))) |
700 | (format #t "Building for ~a~%" system) |
701 | (invoke "./configure" system "-prefix" |
702 | (assoc-ref outputs "out"))) |
703 | #t)) |
704 | (add-after 'install 'install-lib |
705 | (lambda* (#:key outputs #:allow-other-keys) |
706 | (for-each |
707 | (lambda (file) |
708 | (install-file |
709 | file |
710 | (string-append |
711 | (assoc-ref outputs "out") |
712 | "/lib/coq/user-contrib/compcert/" (dirname file)))) |
713 | (find-files "." ".*.vo$")) |
714 | #t))) |
715 | #:tests? #f)) |
716 | (native-inputs |
717 | `(("ocaml" ,ocaml-fix) |
718 | ("coq" ,coq-8.7))) |
719 | (inputs |
720 | `(("menhir" ,ocaml-menhir-fix))) |
721 | (home-page "http://compcert.inria.fr") |
722 | (synopsis "Certified C compiler") |
723 | (description "CompCert is a certified (with coq) C compiler. Warning: this |
724 | package is not free software!") |
725 | ;; actually the "INRIA Non-Commercial License Agreement" |
726 | ;; a non-free license. |
727 | (license (license:non-copyleft "file:///LICENSE")))) |
728 | |
729 | (define-public cubicle |
730 | (package |
731 | (name "cubicle") |
732 | (version "1.1.1") |
733 | (source (origin |
734 | (method url-fetch) |
735 | (uri (string-append "http://cubicle.lri.fr/cubicle-" |
736 | version ".tar.gz")) |
737 | (sha256 |
738 | (base32 |
739 | "1sny9c4fm14k014pk62ibpwbrjjirkx8xmhs9jg7q1hk7y7x3q2h")))) |
740 | (build-system gnu-build-system) |
741 | (native-inputs |
742 | `(("ocaml" ,ocaml) |
743 | ("which" ,which))) |
744 | (propagated-inputs |
745 | `(("z3" ,z3))) |
746 | (arguments |
747 | `(#:configure-flags (list "--with-z3") |
748 | #:tests? #f |
749 | #:phases |
750 | (modify-phases %standard-phases |
751 | (add-before 'configure 'configure-for-release |
752 | (lambda _ |
753 | (substitute* "Makefile.in" |
754 | (("SVNREV=") "#SVNREV=")))) |
755 | (add-before 'configure 'fix-/bin/sh |
756 | (lambda _ |
757 | (substitute* "configure" |
758 | (("/bin/sh") (which "sh"))))) |
759 | (add-before 'configure 'fix-smt-z3wrapper.ml |
760 | (lambda _ |
761 | (substitute* "Makefile.in" |
762 | (("\\\\n") ""))))))) |
763 | (home-page "http://cubicle.lri.fr/") |
764 | (synopsis "Model checker for array-based systems") |
765 | (description "Cubicle is an open source model checker for verifying safety |
766 | properties of array-based systems. This is a syntactically restricted class of |
767 | parametrized transition systems with states represented as arrays indexed by an |
768 | arbitrary number of processes. Cache coherence protocols and mutual exclusion |
769 | algorithms are typical examples of such systems.") |
770 | (license license:asl2.0))) |
771 | |
772 | (define-public ocaml-c2newspeak |
773 | (package |
774 | (name "ocaml-c2newspeak") |
775 | (version "1") |
776 | (source (origin |
777 | (method git-fetch) |
778 | (uri (git-reference |
779 | (url "https://github.com/airbus-seclab/c2newspeak") |
780 | (commit "c97fd380111a49fa7baeb9e49c45238fca627492"))) |
781 | (file-name (string-append name "-" version)) |
782 | (sha256 |
783 | (base32 |
784 | "0fxh868s5jraq61mnig9ilhyjzsq4iw32f20zh3982naanp4p8r6")))) |
785 | (build-system ocaml-build-system) |
786 | (arguments |
787 | `(#:test-target "check" |
788 | #:tests? #f |
789 | #:phases |
790 | (modify-phases %standard-phases |
791 | (delete 'configure) |
792 | (add-after 'install 'install-bin |
793 | (lambda* (#:key outputs #:allow-other-keys) |
794 | (install-file "bin/c2newspeak" (string-append (assoc-ref outputs "out") "/bin"))))))) |
795 | (home-page "https://github.com/airbus-seclab/c2newspeak") |
796 | (synopsis "") |
797 | (description "") |
798 | (license license:lgpl2.1+))) |
799 | |
800 | (define-public ocaml-bincat |
801 | (package |
802 | (name "ocaml-bincat") |
803 | (version "0.8.1") |
804 | (source (origin |
805 | (method url-fetch) |
806 | (uri (string-append "https://github.com/airbus-seclab/bincat/archive/v" |
807 | version ".tar.gz")) |
808 | (file-name (string-append name "-" version ".tar.gz")) |
809 | (sha256 |
810 | (base32 |
811 | "1ncwm1h428x1bs4sq7ql1isrkhw0angglsa9hnsvhhw2i1jsdk7j")))) |
812 | (build-system ocaml-build-system) |
813 | (arguments |
814 | `(#:tests? #f; disabled for now |
815 | #:validate-runpath? #f; disabled for now |
816 | #:make-flags |
817 | (list (string-append "PREFIX=" (assoc-ref %outputs "out")) |
818 | "LDCONFIG=true" |
819 | (string-append "CFLAGS+=-I " (assoc-ref %build-inputs "ocaml") |
820 | "/lib/ocaml")) |
821 | #:phases |
822 | (modify-phases %standard-phases |
823 | (delete 'configure) |
824 | (add-before 'build 'python-path |
825 | (lambda* (#:key outputs #:allow-other-keys) |
826 | (setenv "PYTHONPATH" (string-append (getenv "PYTHONPATH") |
827 | ":../python:" |
828 | (assoc-ref outputs "out") |
829 | "/lib/python2.7/site-packages/")) |
830 | #t)) |
831 | (add-before 'build 'fix-makefiles |
832 | (lambda _ |
833 | (substitute* "ocaml/src/Makefile" |
834 | (("GITVERSION:=.*") "GITVERSION:=0.8.1\n")) |
835 | (substitute* "python/Makefile" |
836 | (("./setup.py install") "./setup.py install --prefix=$(PREFIX)")) |
837 | #t)) |
838 | (add-before 'check 'fix-test |
839 | (lambda _ |
840 | (setenv "PATH" (string-append (getenv "PATH") ":" (getcwd) "/ocaml/src")) |
841 | ;; Remove tests that require an armv8 compiler |
842 | (substitute* "test/Makefile" |
843 | (("eggloader_armv8 eggloader_armv7 eggloader_armv7thumb") "")) |
844 | (chmod "test/eggloader_x86" #o755) |
845 | #t)) |
846 | (add-before 'install 'install-python-dir |
847 | (lambda* (#:key outputs #:allow-other-keys) |
848 | (mkdir-p (string-append (assoc-ref outputs "out") |
849 | "/lib/python2.7/site-packages/"))))))) |
850 | (inputs |
851 | `(("c2newspeak" ,ocaml-c2newspeak) |
852 | ("zarith" ,ocaml-zarith) |
853 | ("menhir" ,ocaml-menhir) |
854 | ("ocamlgraph" ,ocaml-graph) |
855 | ("ocaml-cppo" ,ocaml-cppo) |
856 | ("ocaml-ppx-tools" ,ocaml-ppx-tools) |
857 | ("gmp" ,gmp))) |
858 | (native-inputs |
859 | `(("python" ,python-2) |
860 | ("pytest" ,python2-pytest) |
861 | ("sphinx" ,python2-sphinx) |
862 | ("nasm" ,nasm))) |
863 | (home-page "https://github.com/airbus-seclab/bincat") |
864 | (synopsis "") |
865 | (description "") |
866 | (license license:lgpl2.1+))) |
867 | |
868 | (define-public ocaml-ocplib-simplex |
869 | (package |
870 | (name "ocaml-ocplib-simplex") |
871 | (version "0.4") |
872 | (source (origin |
873 | (method url-fetch) |
874 | (uri (string-append "https://github.com/OCamlPro-Iguernlala/" |
875 | "ocplib-simplex/archive/v" version ".tar.gz")) |
876 | (sha256 |
877 | (base32 |
878 | "0y6q4bgly7fisdklriww48aknqf2vg4dphr7wwnd1wh80l4anzg1")))) |
879 | (build-system gnu-build-system) |
880 | (arguments |
881 | `(#:tests? #f; Compilation error |
882 | #:phases |
883 | (modify-phases %standard-phases |
884 | (add-after 'unpack 'autoreconf |
885 | (lambda _ |
886 | (invoke "autoreconf" "-fiv") |
887 | #t)) |
888 | (add-before 'install 'mkdir |
889 | (lambda* (#:key outputs #:allow-other-keys) |
890 | (let* ((out (assoc-ref outputs "out")) |
891 | (lib (string-append out "/lib"))) |
892 | (mkdir-p lib) |
893 | #t)))))) |
894 | (native-inputs |
895 | `(("autoconf" ,autoconf) |
896 | ("automake" ,automake) |
897 | ("ocaml" ,ocaml) |
898 | ("ocaml-findlib" ,ocaml-findlib) |
899 | ("which" ,which))) |
900 | (home-page "") |
901 | (synopsis "") |
902 | (description "") |
903 | ; lgpl2.1+ with linking exception |
904 | (license license:lgpl2.1+))) |
905 | |
906 | (define-public frama-c |
907 | (package |
908 | (name "frama-c") |
909 | (version "20171101") |
910 | (source (origin |
911 | (method url-fetch) |
912 | (uri (string-append "http://frama-c.com/download/frama-c-Sulfur-" |
913 | version ".tar.gz")) |
914 | (sha256 |
915 | (base32 |
916 | "1vwjfqmm1r36gkybsy3a7m89q5zicf4rnz5vlsn9imnpjpl9gjw1")))) |
917 | (build-system ocaml-build-system) |
918 | (arguments |
919 | `(#:tests? #f; for now |
920 | #:phases |
921 | (modify-phases %standard-phases |
922 | (add-before 'configure 'export-shell |
923 | (lambda* (#:key inputs #:allow-other-keys) |
924 | (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash") |
925 | "/bin/sh"))))))) |
926 | (inputs |
927 | `(("gmp" ,gmp) |
928 | ("ocaml-graph" ,ocaml-graph) |
929 | ("ocaml-zarith" ,ocaml-zarith))) |
930 | (home-page "") |
931 | (synopsis "") |
932 | (description "") |
933 | (license license:lgpl2.1+))) |
934 | |
935 | (define-public opam2 |
936 | (package |
937 | (inherit opam) |
938 | (version "2.0.0") |
939 | (source (origin |
940 | (method url-fetch) |
941 | ;; Use the '-full' version, which includes all the dependencies. |
942 | (uri (string-append |
943 | "https://github.com/ocaml/opam/releases/download/" |
944 | version "/opam-full-" version ".tar.gz") |
945 | ;; (string-append "https://github.com/ocaml/opam/archive/" |
946 | ;; version ".tar.gz") |
947 | ) |
948 | (sha256 |
949 | (base32 |
950 | "09gdpxiqmyr6z78l85d7pwhiwrycdi2xi1b2mafqr1sk9z5lzbcx")))))) |
951 |