Merge branch 'master' into core-updates

1 files changed, 285 insertions, 43 deletions

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 2b4821ed42..5baf24cac0 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -1,6 +1,6 @@
 ;;; GNU Guix --- Functional package management for GNU
 ;;; Copyright © 2013 Cyril Roelandt <tipecaml@gmail.com>
-;;; Copyright © 2014 Mark H Weaver <mhw@netris.org>
+;;; Copyright © 2014, 2015 Mark H Weaver <mhw@netris.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -18,11 +18,20 @@
 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (gnu packages ocaml)
-  #:use-module (guix licenses)
+  #:use-module ((guix licenses) #:hide (zlib))
   #:use-module (guix packages)
   #:use-module (guix download)
+  #:use-module (guix utils)
   #:use-module (guix build-system gnu)
   #:use-module (gnu packages)
+  #:use-module (gnu packages base)
+  #:use-module (gnu packages emacs)
+  #:use-module (gnu packages texinfo)
+  #:use-module (gnu packages pkg-config)
+  #:use-module (gnu packages compression)
+  #:use-module (gnu packages commencement)
+  #:use-module (gnu packages xorg)
+  #:use-module (gnu packages texlive)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages python)
   #:use-module (gnu packages ncurses)
@@ -32,56 +41,94 @@
 (define-public ocaml
   (package
     (name "ocaml")
-    (version "4.00.1")
+    (version "4.02.1")
     (source (origin
-             (method url-fetch)
-             (uri (string-append
-                   "http://caml.inria.fr/pub/distrib/ocaml-4.00/ocaml-"
-                   version ".tar.gz"))
-             (sha256
-              (base32
-               "0yp86napnvbi2jgxr6bk1235bmjdclgzrzgq4mhwv87l7dymr3dl"))))
+              (method url-fetch)
+              (uri (string-append
+                    "http://caml.inria.fr/pub/distrib/ocaml-"
+                    (version-major+minor version)
+                    "/ocaml-" version ".tar.xz"))
+              (sha256
+               (base32
+                "1p7lqvh64xpykh99014mz21q8fs3qyjym2qazhhbq8scwldv1i38"))))
     (build-system gnu-build-system)
+    (native-inputs
+     `(("perl" ,perl)
+       ("pkg-config" ,pkg-config)))
+    (inputs
+     `(("libx11" ,libx11)
+       ("gcc:lib" ,gcc-final "lib") ; for libiberty, needed for objdump support
+       ("zlib" ,zlib)))             ; also needed for objdump support
     (arguments
-       `(#:modules ((guix build gnu-build-system)
-                    (guix build utils)
-                    (srfi srfi-1))
-         #:phases (alist-replace
-                   'configure
-                   (lambda* (#:key outputs #:allow-other-keys)
-                     ;; OCaml uses "-prefix <prefix>" rather than the usual
-                     ;; "--prefix=<prefix>".
-                     (let ((out (assoc-ref outputs "out")))
-                      (zero? (system* "./configure" "-prefix" out
-                                      "-mandir"
-                                      (string-append out "/share/man")))))
-                   (alist-replace
-                    'build
-                    (lambda* (#:key outputs #:allow-other-keys)
-                      ;; "make" does not do anything, we must use
-                      ;; "make world.opt".
-                      (zero? (system* "make" "world.opt")))
-                    (alist-replace
-                     'check-after-install
-                     (lambda* (#:key outputs #:allow-other-keys)
-                       ;; There does not seem to be a "check" or "test" target.
-                       (zero? (system "cd testsuite && make all")))
-                     (let ((check (assq-ref %standard-phases 'check)))
-                      ;; OCaml assumes that "make install" is run before
-                      ;; launching the tests.
-                      (alist-cons-after
-                       'install 'check-after-install
-                       check
-                       (alist-delete 'check %standard-phases))))))))
-    (inputs `(("perl" ,perl)))
-    (home-page "http://caml.inria.fr/")
+     `(#:modules ((guix build gnu-build-system)
+                  (guix build utils)
+                  (web server))
+       #:phases
+       (modify-phases %standard-phases
+         (add-after 'unpack 'patch-/bin/sh-references
+                    (lambda* (#:key inputs #:allow-other-keys)
+                      (let* ((sh (string-append (assoc-ref inputs "bash")
+                                                "/bin/sh"))
+                             (quoted-sh (string-append "\"" sh "\"")))
+                        (with-fluids ((%default-port-encoding #f))
+                          (for-each (lambda (file)
+                                      (substitute* file
+                                        (("\"/bin/sh\"")
+                                         (begin
+                                           (format (current-error-port) "\
+patch-/bin/sh-references: ~a: changing `\"/bin/sh\"' to `~a'~%"
+                                                   file quoted-sh)
+                                           quoted-sh))))
+                                    (find-files "." "\\.ml$"))
+                          #t))))
+         (replace 'configure
+                  (lambda* (#:key outputs #:allow-other-keys)
+                    (let* ((out (assoc-ref outputs "out"))
+                           (mandir (string-append out "/share/man")))
+                      ;; Custom configure script doesn't recognize
+                      ;; --prefix=<PREFIX> syntax (with equals sign).
+                      (zero? (system* "./configure"
+                                      "--prefix" out
+                                      "--mandir" mandir)))))
+         (replace 'build
+                  (lambda _
+                    (zero? (system* "make" "-j" (number->string
+                                                 (parallel-job-count))
+                                    "world.opt"))))
+         (delete 'check)
+         (add-after 'install 'check
+                    (lambda _
+                      (with-directory-excursion "testsuite"
+                        (zero? (system* "make" "all")))))
+         (add-before 'check 'prepare-socket-test
+                     (lambda _
+                       (format (current-error-port)
+                               "Spawning local test web server on port 8080~%")
+                       (when (zero? (primitive-fork))
+                         (run-server (lambda (request request-body)
+                                       (values '((content-type . (text/plain)))
+                                               "Hello!"))
+                                     'http '(#:port 8080)))
+                       (let ((file "testsuite/tests/lib-threads/testsocket.ml"))
+                         (format (current-error-port)
+                                 "Patching ~a to use localhost port 8080~%"
+                                 file)
+                         (substitute* file
+                           (("caml.inria.fr") "localhost")
+                           (("80") "8080")
+                           (("HTTP1.0") "HTTP/1.0"))
+                         #t))))))
+    (home-page "https://ocaml.org/")
     (synopsis "The OCaml programming language")
     (description
      "OCaml is a general purpose industrial-strength programming language with
 an emphasis on expressiveness and safety.  Developed for more than 20 years at
 Inria it benefits from one of the most advanced type systems and supports
 functional, imperative and object-oriented styles of programming.")
-    (license (list qpl gpl2))))
+    ;; The compiler is distributed under qpl1.0 with a change to choice of
+    ;; law: the license is governed by the laws of France.  The library is
+    ;; distributed under lgpl2.0.
+    (license (list qpl lgpl2.0))))
 
 (define-public opam
   (package
@@ -143,3 +190,198 @@ Git-friendly development workflow.")
 
     ;; The 'LICENSE' file waives some requirements compared to LGPLv3.
     (license lgpl3)))
+
+(define-public camlp5
+  (package
+    (name "camlp5")
+    (version "6.12")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://camlp5.gforge.inria.fr/distrib/src/"
+                                  name "-" version ".tgz"))
+              (sha256
+               (base32
+                "00jwgp6w4g64lfqjx77xziy532091fy00c42fsy0b4i892rch5mp"))))
+    (build-system gnu-build-system)
+    (inputs
+     `(("ocaml" ,ocaml)))
+    (arguments
+     `(#:tests? #f  ; XXX TODO figure out how to run the tests
+       #: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")))
+                      ;; Custom configure script doesn't recognize
+                      ;; --prefix=<PREFIX> syntax (with equals sign).
+                      (zero? (system* "./configure"
+                                      "--prefix" out
+                                      "--mandir" mandir)))))
+         (replace 'build
+                  (lambda _
+                    (zero? (system* "make" "-j" (number->string
+                                                 (parallel-job-count))
+                                    "world.opt")))))))
+    (home-page "http://camlp5.gforge.inria.fr/")
+    (synopsis "Pre-processor Pretty Printer for OCaml")
+    (description
+     "Camlp5 is a Pre-Processor-Pretty-Printer for Objective Caml.  It offers
+tools for syntax (Stream Parsers and Grammars) and the ability to modify the
+concrete syntax of the language (Quotations, Syntax Extensions).")
+    ;; Most files are distributed under bsd-3, but ocaml_stuff/* is under qpl.
+    (license (list bsd-3 qpl))))
+
+(define-public hevea
+  (package
+    (name "hevea")
+    (version "2.23")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://hevea.inria.fr/distri/"
+                                  name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "1f9pj48518ixhjxbviv2zx27v4anp92zgg3x704g1s5cki2w33nv"))))
+    (build-system gnu-build-system)
+    (inputs
+     `(("ocaml" ,ocaml)))
+    (arguments
+     `(#:tests? #f  ; no test suite
+       #:make-flags (list (string-append "PREFIX=" %output))
+       #:phases (modify-phases %standard-phases
+                  (delete 'configure))))
+    (home-page "http://hevea.inria.fr/")
+    (synopsis "LaTeX to HTML translator")
+    (description
+     "HeVeA is a LaTeX to HTML translator that generates modern HTML 5.  It is
+written in Objective Caml.")
+    (license qpl)))
+
+(define-public coq
+  (package
+    (name "coq")
+    (version "8.4pl6")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://coq.inria.fr/distrib/V" version
+                                  "/files/" name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "1mpbj4yf36kpjg2v2sln12i8dzqn8rag6fd07hslj2lpm4qs4h55"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("texlive" ,texlive)
+       ("hevea" ,hevea)))
+    (inputs
+     `(("ocaml" ,ocaml)
+       ("camlp5" ,camlp5)))
+    (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)\""))
+                      (zero? (system* "./configure"
+                                      "--prefix" out
+                                      "--mandir" mandir
+                                      "--browser" browser)))))
+         (replace 'build
+                  (lambda _
+                    (zero? (system* "make" "-j" (number->string
+                                                 (parallel-job-count))
+                                    "world"))))
+         (delete 'check)
+         (add-after 'install 'check
+                    (lambda _
+                      (with-directory-excursion "test-suite"
+                        (zero? (system* "make"))))))))
+    (home-page "https://coq.inria.fr")
+    (synopsis "Proof assistant for higher-order logic")
+    (description
+     "Coq is a proof assistant for higher-order logic, which allows the
+development of computer programs consistent with their formal specification.
+It is developed using Objective Caml and Camlp5.")
+    ;; The code is distributed under lgpl2.1.
+    ;; Some of the documentation is distributed under opl1.0+.
+    (license (list lgpl2.1 opl1.0+))))
+
+(define-public proof-general
+  (package
+    (name "proof-general")
+    (version "4.2")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "http://proofgeneral.inf.ed.ac.uk/releases/"
+                    "ProofGeneral-" version ".tgz"))
+              (sha256
+               (base32
+                "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("which" ,which)
+       ("emacs" ,emacs-no-x)
+       ("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))
+       #: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))
+                        (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/")
+    (description "Generic front-end for proof assistants based on Emacs")
+    (synopsis
+     "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 gpl2+)))