guix-more

ocaml.scm

;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2017 Julien Lepiller <julien@lepiller.eu>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.

(define-module (more packages ocaml)
  #:use-module (guix packages)
  #:use-module (guix download)
  #:use-module (guix git-download)
  #:use-module (guix utils)
  #:use-module (guix build-system gnu)
  #:use-module (guix build-system ocaml)
  #:use-module ((guix licenses) #:prefix license:)
  #:use-module (gnu packages)
  #:use-module (gnu packages assembly)
  #:use-module (gnu packages autotools)
  #:use-module (gnu packages base)
  #:use-module (gnu packages bison)
  #:use-module (gnu packages boost)
  #:use-module (gnu packages check)
  #:use-module (gnu packages emacs)
  #:use-module (gnu packages flex)
  #:use-module (gnu packages llvm)
  #:use-module (gnu packages m4)
  #:use-module (gnu packages maths)
  #:use-module (gnu packages multiprecision)
  #:use-module (gnu packages ocaml)
  #:use-module (gnu packages perl)
  #:use-module (gnu packages pkg-config)
  #:use-module (gnu packages protobuf)
  #:use-module (gnu packages python)
  #:use-module (gnu packages tex)
  #:use-module (gnu packages texinfo)
  #:use-module (more packages smt)
  #:use-module (ice-9 match))

(define (ocaml-forge-uri name version file-number)
  (string-append "https://forge.ocamlcore.org/frs/download.php/"
                 (number->string file-number) "/" name "-" version
                 ".tar.gz"))

(define-public proof-general2
  (package
    (name "proof-general2")
    (version "4.4")
    (source (origin
              (method url-fetch)
              (uri (string-append
                    "https://github.com/ProofGeneral/PG/archive/v"
                    version ".tar.gz"))
              (file-name (string-append name "-" version ".tar.gz"))
              (sha256
               (base32
                "0zif2fv6mm4pv75nh10q3p37n293495rvx470bx7ma382zc3d8hv"))))
    (build-system gnu-build-system)
    (native-inputs
     `(("which" ,which)
       ("emacs" ,emacs-minimal)
       ("texinfo" ,texinfo)))
    (inputs
     `(("host-emacs" ,emacs)
       ("perl" ,perl)
       ("coq" ,coq)))
    (arguments
     `(#:tests? #f  ; no check target
       #:make-flags (list (string-append "PREFIX=" %output)
                          (string-append "DEST_PREFIX=" %output)
                          "-j1")
       #:modules ((guix build gnu-build-system)
                  (guix build utils)
                  (guix build emacs-utils))
       #:imported-modules (,@%gnu-build-system-modules
                           (guix build emacs-utils))
       #:phases
       (modify-phases %standard-phases
         (delete 'configure)
         (add-after 'unpack 'disable-byte-compile-error-on-warn
                    (lambda _
                      (substitute* "Makefile"
                        (("\\(setq byte-compile-error-on-warn t\\)")
                         "(setq byte-compile-error-on-warn nil)"))
                      #t))
         (add-after 'unpack 'patch-hardcoded-paths
                    (lambda* (#:key inputs outputs #:allow-other-keys)
                      (let ((out   (assoc-ref outputs "out"))
                            (coq   (assoc-ref inputs "coq"))
                            (emacs (assoc-ref inputs "host-emacs")))
                        (define (coq-prog name)
                          (string-append coq "/bin/" name))
                        (substitute* "pgshell/pgshell.el"
                          (("/bin/sh") (which "sh")))
                        ;(emacs-substitute-variables "coq/coq.el"
                        ;  ("coq-prog-name"           (coq-prog "coqtop"))
                        ;  ("coq-compiler"            (coq-prog "coqc"))
                        ;  ("coq-dependency-analyzer" (coq-prog "coqdep")))
                        (substitute* "Makefile"
                          (("/sbin/install-info") "install-info"))
                        (substitute* "bin/proofgeneral"
                          (("^PGHOMEDEFAULT=.*" all)
                           (string-append all
                                          "PGHOME=$PGHOMEDEFAULT\n"
                                          "EMACS=" emacs "/bin/emacs")))
                        #t))))))
         ;(add-after 'unpack 'clean
         ;           (lambda _
         ;             ;; Delete the pre-compiled elc files for Emacs 23.
         ;             (zero? (system* "make" "clean"))))
         ;(add-after 'install 'install-doc
         ;           (lambda* (#:key make-flags #:allow-other-keys)
         ;             ;; XXX FIXME avoid building/installing pdf files,
         ;             ;; due to unresolved errors building them.
         ;             (substitute* "Makefile"
         ;               ((" [^ ]*\\.pdf") ""))
         ;             (zero? (apply system* "make" "install-doc"
         ;                           make-flags)))))))
    (home-page "http://proofgeneral.inf.ed.ac.uk/")
    (synopsis "Generic front-end for proof assistants based on Emacs")
    (description
     "Proof General is a major mode to turn Emacs into an interactive proof
assistant to write formal mathematical proofs using a variety of theorem
provers.")
    (license license:gpl2+)))

(define-public coq-8.6
  (package
    (inherit coq)
    (name "coq")
    (version "8.6.1")
    (source (origin
              (method url-fetch)
              (uri (string-append "https://github.com/coq/coq/archive/V"
                                  version ".tar.gz"))
              (file-name (string-append name "-" version ".tar.gz"))
              (sha256
               (base32
                "02nm5sn79hrb9fdmkhyclk80jydadf4jcafmr3idwr5h4z56qbms"))))
    (arguments
     `(#:phases
       (modify-phases %standard-phases
         (replace 'configure
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (mandir (string-append out "/share/man"))
                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
               (invoke "./configure"
                       "-prefix" out
                       "-mandir" mandir
                       "-browser" browser
                       "-coqide" "opt"))
             #t))
         (replace 'build
           (lambda* (#:key inputs #:allow-other-keys)
             (substitute* "ide/ideutils.ml"
               (("Bytes.unsafe_to_string read_string") "read_string"))
             (invoke "make" "-j" (number->string
                                  (parallel-job-count))
                     "world")
             #t))
         (delete 'check)
         (add-after 'install 'check
           (lambda _
             (with-directory-excursion "test-suite"
               (invoke "make"))
             #t)))))))

(define-public coq-8.7
  (package
    (inherit coq)
    (name "coq")
    (version "8.7.2")
    (source (origin
              (method url-fetch)
              (uri (string-append "https://github.com/coq/coq/archive/V"
                                  version ".tar.gz"))
              (file-name (string-append name "-" version ".tar.gz"))
              (sha256
               (base32
                "1lkqvs7ayzv5kkg26y837pg0d6r2b5hbjxl71ba93f39kybw69gg"))))
    (arguments
     `(#:phases
       (modify-phases %standard-phases
         (replace 'configure
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (mandir (string-append out "/share/man"))
                    (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
               (invoke "./configure"
                       "-prefix" out
                       "-mandir" mandir
                       "-browser" browser
                       "-coqide" "opt"))
             #t))
         (replace 'build
           (lambda* (#:key inputs #:allow-other-keys)
             (substitute* "ide/ideutils.ml"
               (("Bytes.unsafe_to_string read_string") "read_string"))
             (invoke "make" "-j" (number->string
                                  (parallel-job-count))
                     (string-append
                       "USERFLAGS=-I "
                       (assoc-ref inputs "ocaml-num")
                       "/lib/ocaml/site-lib")
                     "world")
             #t))
         (delete 'check)
         (add-after 'install 'check
           (lambda _
             (with-directory-excursion "test-suite"
               ;; These two tests fail.
               ;; This one fails because the output is not formatted as expected.
               (delete-file-recursively "coq-makefile/timing")
               ;; This one fails because we didn't build coqtop.byte.
               (delete-file-recursively "coq-makefile/findlib-package")
               (invoke "make"))
             #t)))))))

(define-public coq-bignums-8.7
  (package
    (inherit coq-bignums)
    (name "coq-bignums")
    (version "8.7.0")
    (source (origin
              (method url-fetch)
              (uri (string-append "https://github.com/coq/bignums/archive/V"
                                  version ".tar.gz"))
              (file-name (string-append name "-" version ".tar.gz"))
              (sha256
               (base32
                "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx"))))
    (native-inputs
     `(("ocaml" ,ocaml)
       ("coq-8.7" ,coq-8.7)))
    (inputs
     `(("camlp5" ,camlp5)))))

(define-public ppsimpl
  (package
    (name "ppsimpl")
    (version "8.7")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                     (url "https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git")
                     (commit "86255a47568df58767d1d8e0b9e2da31cf73a5fc")))
              (file-name (string-append name "-" version))
              (sha256
               (base32
                "0h509w43j2wd2pyx04k3xfd0bsbmqscwqvhf8whzc3cxzl4j6vvq"))))
              ;(uri "https://gforge.inria.fr/frs/download.php/file/37615/ppsimpl-09-07-2018.tar.gz")
              ;(sha256
              ; (base32
              ;  "010zgskc1wd5v6wmmyxaapvwxjlgbdqqiks2dvf6llx03b07ak59"))))
    (build-system gnu-build-system)
    (arguments
     `(#:test-target "test"
       #:configure-flags
       (list "-R" (string-append (assoc-ref %build-inputs "compcert") "/lib/coq/user-contrib/compcert") "compcert")
       #:make-flags (list "COQC=coqc -R src PP -I src"
                          (string-append
                            "COQLIBINSTALL="
                            (assoc-ref %outputs "out")
                            "/lib/coq/user-contrib"))))
    (inputs
     `(("coq-bignums-8.7" ,coq-bignums-8.7)
       ("compcert" ,compcert)))
    (native-inputs
     `(("coq-8.7" ,coq-8.7)
       ("ocaml" ,ocaml)
       ("ocaml-findlib" ,ocaml-findlib)
       ("camlp4" ,camlp4)
       ("camlp5" ,camlp5)
       ("which" ,which)))
    (home-page "")
    (synopsis "")
    (description "")
    ;; No declared license -> all rights reserved
    (license #f)))

(define-public compcert
  (package
    (name "compcert")
    (version "3.3")
    (source (origin
              (method url-fetch)
              (uri (string-append "http://compcert.inria.fr/release/compcert-"
                                  version ".tgz"))
              (sha256
               (base32
                "16xrqcwak1v1fk5ndx6jf1yvxv3adsr7p7z34gfm2mpggxnq0xwn"))))
    (build-system gnu-build-system)
    (arguments
     `(#:phases
       (modify-phases %standard-phases
         (replace 'configure
           (lambda* (#:key outputs #:allow-other-keys)
             (let ((system ,(match (or (%current-target-system) (%current-system))
                              ("x86_64-linux" "x86_64-linux")
                              ("i686-linux" "x86_32-linux")
                              ("armhf-linux" "arm-linux"))))
               (format #t "Building for ~a~%" system)
               (invoke "./configure" system "-prefix"
                       (assoc-ref outputs "out")))
             #t))
         (add-after 'install 'install-lib
           (lambda* (#:key outputs #:allow-other-keys)
             (for-each
               (lambda (file)
                 (install-file
                   file
                   (string-append
                     (assoc-ref outputs "out")
                     "/lib/coq/user-contrib/compcert/" (dirname file))))
               (find-files "." ".*.vo$"))
             #t)))
       #:tests? #f))
    (native-inputs
     `(("ocaml" ,ocaml)
       ("coq" ,coq-8.7)))
    (inputs
     `(("menhir" ,ocaml-menhir-fix)))
    (home-page "http://compcert.inria.fr")
    (synopsis "Certified C compiler")
    (description "CompCert is a certified (with coq) C compiler.  Warning: this
package is not free software!")
    ;; actually the "INRIA Non-Commercial License Agreement"
    ;; a non-free license.
    (license (license:non-copyleft "file:///LICENSE"))))

(define-public ocaml-c2newspeak
  (package
    (name "ocaml-c2newspeak")
    (version "1")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                     (url "https://github.com/airbus-seclab/c2newspeak")
                     (commit "c97fd380111a49fa7baeb9e49c45238fca627492")))
              (file-name (string-append name "-" version))
              (sha256
               (base32
                "0fxh868s5jraq61mnig9ilhyjzsq4iw32f20zh3982naanp4p8r6"))))
    (build-system ocaml-build-system)
    (arguments
     `(#:test-target "check"
       #:tests? #f
       #:phases
       (modify-phases %standard-phases
         (delete 'configure)
         (add-after 'install 'install-bin
           (lambda* (#:key outputs #:allow-other-keys)
             (install-file "bin/c2newspeak" (string-append (assoc-ref outputs "out") "/bin")))))))
    (home-page "https://github.com/airbus-seclab/c2newspeak")
    (synopsis "")
    (description "")
    (license license:lgpl2.1+)))

(define-public ocaml-bincat
  (package
    (name "ocaml-bincat")
    (version "0.8.1")
    (source (origin
              (method url-fetch)
              (uri (string-append "https://github.com/airbus-seclab/bincat/archive/v"
                                  version ".tar.gz"))
              (file-name (string-append name "-" version ".tar.gz"))
              (sha256
               (base32
                "1ncwm1h428x1bs4sq7ql1isrkhw0angglsa9hnsvhhw2i1jsdk7j"))))
    (build-system ocaml-build-system)
    (arguments
     `(#:tests? #f; disabled for now
       #:validate-runpath? #f; disabled for now
       #:make-flags
       (list (string-append "PREFIX=" (assoc-ref %outputs "out"))
             "LDCONFIG=true"
             (string-append "CFLAGS+=-I " (assoc-ref %build-inputs "ocaml")
                            "/lib/ocaml"))
       #:phases
       (modify-phases %standard-phases
         (delete 'configure)
         (add-before 'build 'python-path
           (lambda* (#:key outputs #:allow-other-keys)
             (setenv "PYTHONPATH" (string-append (getenv "PYTHONPATH")
                                                 ":../python:"
                                                 (assoc-ref outputs "out")
                                                 "/lib/python2.7/site-packages/"))
             #t))
         (add-before 'build 'fix-makefiles
           (lambda _
             (substitute* "ocaml/src/Makefile"
               (("GITVERSION:=.*") "GITVERSION:=0.8.1\n"))
             (substitute* "python/Makefile"
               (("./setup.py install") "./setup.py install --prefix=$(PREFIX)"))
             #t))
         (add-before 'check 'fix-test
           (lambda _
             (setenv "PATH" (string-append (getenv "PATH") ":" (getcwd) "/ocaml/src"))
             ;; Remove tests that require an armv8 compiler
             (substitute* "test/Makefile"
               (("eggloader_armv8 eggloader_armv7 eggloader_armv7thumb") ""))
             (chmod "test/eggloader_x86" #o755)
             #t))
         (add-before 'install 'install-python-dir
           (lambda* (#:key outputs #:allow-other-keys)
             (mkdir-p (string-append (assoc-ref outputs "out")
                                     "/lib/python2.7/site-packages/")))))))
    (inputs
     `(("c2newspeak" ,ocaml-c2newspeak)
       ("zarith" ,ocaml-zarith)
       ("menhir" ,ocaml-menhir)
       ("ocamlgraph" ,ocaml-graph)
       ("ocaml-cppo" ,ocaml-cppo)
       ("ocaml-ppx-tools" ,ocaml-ppx-tools)
       ("gmp" ,gmp)))
    (native-inputs
     `(("python" ,python-2)
       ("pytest" ,python2-pytest)
       ("sphinx" ,python2-sphinx)
       ("nasm" ,nasm)))
    (home-page "https://github.com/airbus-seclab/bincat")
    (synopsis "")
    (description "")
    (license license:lgpl2.1+)))

(define-public ocaml-ocplib-simplex
  (package
    (name "ocaml-ocplib-simplex")
    (version "0.4")
    (source (origin
              (method url-fetch)
              (uri (string-append "https://github.com/OCamlPro-Iguernlala/"
                                  "ocplib-simplex/archive/v" version ".tar.gz"))
              (sha256
               (base32
                "0y6q4bgly7fisdklriww48aknqf2vg4dphr7wwnd1wh80l4anzg1"))))
    (build-system gnu-build-system)
    (arguments
     `(#:tests? #f; Compilation error
       #:phases
       (modify-phases %standard-phases
         (add-after 'unpack 'autoreconf
           (lambda _
             (invoke "autoreconf" "-fiv")
             #t))
         (add-before 'install 'mkdir
           (lambda* (#:key outputs #:allow-other-keys)
             (let* ((out (assoc-ref outputs "out"))
                    (lib (string-append out "/lib")))
               (mkdir-p lib)
               #t))))))
    (native-inputs
     `(("autoconf" ,autoconf)
       ("automake" ,automake)
       ("ocaml" ,ocaml)
       ("ocaml-findlib" ,ocaml-findlib)
       ("which" ,which)))
    (home-page "")
    (synopsis "")
    (description "")
    ; lgpl2.1+ with linking exception
    (license license:lgpl2.1+)))

(define-public frama-c
  (package
    (name "frama-c")
    (version "20171101")
    (source (origin
              (method url-fetch)
              (uri (string-append "http://frama-c.com/download/frama-c-Sulfur-"
                                  version ".tar.gz"))
              (sha256
               (base32
                "1vwjfqmm1r36gkybsy3a7m89q5zicf4rnz5vlsn9imnpjpl9gjw1"))))
    (build-system ocaml-build-system)
    (arguments
     `(#:tests? #f; for now
       #:phases
       (modify-phases %standard-phases
         (add-before 'configure 'export-shell
           (lambda* (#:key inputs #:allow-other-keys)
             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
                                                   "/bin/sh")))))))
    (inputs
     `(("gmp" ,gmp)
       ("ocaml-graph" ,ocaml-graph)
       ("ocaml-zarith" ,ocaml-zarith)))
    (home-page "")
    (synopsis "")
    (description "")
    (license license:lgpl2.1+)))


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