;;; 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+)))