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