gnu/packages/ocaml.scm

   1 ;;; GNU Guix --- Functional package management for GNU
   2 ;;; Copyright © 2013 Cyril Roelandt <tipecaml@gmail.com>
   3 ;;; Copyright © 2014, 2015 Mark H Weaver <mhw@netris.org>
   4 ;;; Copyright © 2015 Andreas Enge <andreas@enge.fr>
   5 ;;;
   6 ;;; This file is part of GNU Guix.
   7 ;;;
   8 ;;; GNU Guix is free software; you can redistribute it and/or modify it
   9 ;;; under the terms of the GNU General Public License as published by
  10 ;;; the Free Software Foundation; either version 3 of the License, or (at
  11 ;;; your option) any later version.
  12 ;;;
  13 ;;; GNU Guix is distributed in the hope that it will be useful, but
  14 ;;; WITHOUT ANY WARRANTY; without even the implied warranty of
  15 ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  16 ;;; GNU General Public License for more details.
  17 ;;;
  18 ;;; You should have received a copy of the GNU General Public License
  19 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
  20
  21 (define-module (gnu packages ocaml)
  22   #:use-module ((guix licenses) #:hide (zlib))
  23   #:use-module (guix packages)
  24   #:use-module (guix download)
  25   #:use-module (guix utils)
  26   #:use-module (guix build-system gnu)
  27   #:use-module (gnu packages)
  28   #:use-module (gnu packages gcc)
  29   #:use-module (gnu packages gnome)
  30   #:use-module (gnu packages gtk)
  31   #:use-module (gnu packages base)
  32   #:use-module (gnu packages emacs)
  33   #:use-module (gnu packages texinfo)
  34   #:use-module (gnu packages pkg-config)
  35   #:use-module (gnu packages compression)
  36   #:use-module (gnu packages xorg)
  37   #:use-module (gnu packages texlive)
  38   #:use-module (gnu packages perl)
  39   #:use-module (gnu packages python)
  40   #:use-module (gnu packages ncurses)
  41   #:use-module (gnu packages version-control)
  42   #:use-module (gnu packages curl))
  43
  44 (define-public ocaml
  45   (package
  46     (name "ocaml")
  47     (version "4.02.3")
  48     (source (origin
  49               (method url-fetch)
  50               (uri (string-append
  51                     "http://caml.inria.fr/pub/distrib/ocaml-"
  52                     (version-major+minor version)
  53                     "/ocaml-" version ".tar.xz"))
  54               (sha256
  55                (base32
  56                 "1qwwvy8nzd87hk8rd9sm667nppakiapnx4ypdwcrlnav2dz6kil3"))))
  57     (build-system gnu-build-system)
  58     (native-inputs
  59      `(("perl" ,perl)
  60        ("pkg-config" ,pkg-config)))
  61     (inputs
  62      `(("libx11" ,libx11)
  63        ;; For libiberty, needed for objdump support.
  64        ("gcc:lib" ,(canonical-package gcc-4.9) "lib")
  65        ("zlib" ,zlib)))                       ;also needed for objdump support
  66     (arguments
  67      `(#:modules ((guix build gnu-build-system)
  68                   (guix build utils)
  69                   (web server))
  70        #:phases
  71        (modify-phases %standard-phases
  72          (add-after 'unpack 'patch-/bin/sh-references
  73                     (lambda* (#:key inputs #:allow-other-keys)
  74                       (let* ((sh (string-append (assoc-ref inputs "bash")
  75                                                 "/bin/sh"))
  76                              (quoted-sh (string-append "\"" sh "\"")))
  77                         (with-fluids ((%default-port-encoding #f))
  78                           (for-each (lambda (file)
  79                                       (substitute* file
  80                                         (("\"/bin/sh\"")
  81                                          (begin
  82                                            (format (current-error-port) "\
  83 patch-/bin/sh-references: ~a: changing `\"/bin/sh\"' to `~a'~%"
  84                                                    file quoted-sh)
  85                                            quoted-sh))))
  86                                     (find-files "." "\\.ml$"))
  87                           #t))))
  88          (replace 'configure
  89                   (lambda* (#:key outputs #:allow-other-keys)
  90                     (let* ((out (assoc-ref outputs "out"))
  91                            (mandir (string-append out "/share/man")))
  92                       ;; Custom configure script doesn't recognize
  93                       ;; --prefix=<PREFIX> syntax (with equals sign).
  94                       (zero? (system* "./configure"
  95                                       "--prefix" out
  96                                       "--mandir" mandir)))))
  97          (replace 'build
  98                   (lambda _
  99                     (zero? (system* "make" "-j" (number->string
 100                                                  (parallel-job-count))
 101                                     "world.opt"))))
 102          (delete 'check)
 103          (add-after 'install 'check
 104                     (lambda _
 105                       (with-directory-excursion "testsuite"
 106                         (zero? (system* "make" "all")))))
 107          (add-before 'check 'prepare-socket-test
 108                      (lambda _
 109                        (format (current-error-port)
 110                                "Spawning local test web server on port 8080~%")
 111                        (when (zero? (primitive-fork))
 112                          (run-server (lambda (request request-body)
 113                                        (values '((content-type . (text/plain)))
 114                                                "Hello!"))
 115                                      'http '(#:port 8080)))
 116                        (let ((file "testsuite/tests/lib-threads/testsocket.ml"))
 117                          (format (current-error-port)
 118                                  "Patching ~a to use localhost port 8080~%"
 119                                  file)
 120                          (substitute* file
 121                            (("caml.inria.fr") "localhost")
 122                            (("80") "8080")
 123                            (("HTTP1.0") "HTTP/1.0"))
 124                          #t))))))
 125     (home-page "https://ocaml.org/")
 126     (synopsis "The OCaml programming language")
 127     (description
 128      "OCaml is a general purpose industrial-strength programming language with
 129 an emphasis on expressiveness and safety.  Developed for more than 20 years at
 130 Inria it benefits from one of the most advanced type systems and supports
 131 functional, imperative and object-oriented styles of programming.")
 132     ;; The compiler is distributed under qpl1.0 with a change to choice of
 133     ;; law: the license is governed by the laws of France.  The library is
 134     ;; distributed under lgpl2.0.
 135     (license (list qpl lgpl2.0))))
 136
 137 (define-public opam
 138   (package
 139     (name "opam")
 140     (version "1.1.1")
 141     (source (origin
 142               (method url-fetch)
 143               ;; Use the '-full' version, which includes all the dependencies.
 144               (uri (string-append
 145                     "https://github.com/ocaml/opam/releases/download/"
 146                     version "/opam-full-" version ".tar.gz")
 147                ;; (string-append "https://github.com/ocaml/opam/archive/"
 148                ;;                    version ".tar.gz")
 149                )
 150               (sha256
 151                (base32
 152                 "1frzqkx6yn1pnyd9qz3bv3rbwv74bmc1xji8kl41r1dkqzfl3xqv"))))
 153     (build-system gnu-build-system)
 154     (arguments
 155      '(;; Sometimes, 'make -jX' would fail right after ./configure with
 156        ;; "Fatal error: exception End_of_file".
 157        #:parallel-build? #f
 158
 159        ;; For some reason, 'ocp-build' needs $TERM to be set.
 160        #:make-flags '("TERM=screen")
 161        #:test-target "tests"
 162
 163        ;; FIXME: There's an obscure test failure:
 164        ;;   …/_obuild/opam/opam.asm install P1' failed.
 165        #:tests? #f
 166
 167        #:phases (alist-cons-before
 168                  'build 'pre-build
 169                  (lambda* (#:key inputs #:allow-other-keys)
 170                    (let ((bash (assoc-ref inputs "bash")))
 171                      (substitute* "src/core/opamSystem.ml"
 172                        (("\"/bin/sh\"")
 173                         (string-append "\"" bash "/bin/sh\"")))))
 174                  (alist-cons-before
 175                   'check 'pre-check
 176                   (lambda _
 177                     (setenv "HOME" (getcwd))
 178                     (and (system "git config --global user.email guix@gnu.org")
 179                          (system "git config --global user.name Guix")))
 180                   %standard-phases))))
 181     (native-inputs
 182      `(("git" ,git)                               ;for the tests
 183        ("python" ,python)))                       ;for the tests
 184     (inputs
 185      `(("ocaml" ,ocaml)
 186        ("ncurses" ,ncurses)
 187        ("curl" ,curl)))
 188     (home-page "http://opam.ocamlpro.com/")
 189     (synopsis "Package manager for OCaml")
 190     (description
 191      "OPAM is a tool to manage OCaml packages.  It supports multiple
 192 simultaneous compiler installations, flexible package constraints, and a
 193 Git-friendly development workflow.")
 194
 195     ;; The 'LICENSE' file waives some requirements compared to LGPLv3.
 196     (license lgpl3)))
 197
 198 (define-public camlp4
 199   (package
 200     (name "camlp4")
 201     (version "4.02+6")
 202     (source (origin
 203               (method url-fetch)
 204               (uri (string-append "https://github.com/ocaml/camlp4/archive/"
 205                                   version ".tar.gz"))
 206               (sha256
 207                (base32
 208                 "0icdfzhsbgf89925gc8gl3fm8z2xzszzlib0v9dj5wyzkyv3a342"))
 209               (file-name (string-append name "-" version ".tar.gz"))))
 210     (build-system gnu-build-system)
 211     (native-inputs `(("ocaml" ,ocaml)
 212                      ("which" ,which)))
 213     (inputs `(("ocaml" ,ocaml)))
 214     (arguments
 215      '(#:tests? #f                                ;no documented test target
 216        #:phases (modify-phases %standard-phases
 217                   (replace
 218                    'configure
 219                    (lambda* (#:key outputs #:allow-other-keys)
 220                      ;; This is a home-made 'configure' script.
 221                      (let ((out (assoc-ref outputs "out")))
 222                        (zero? (system* "./configure"
 223                                        (string-append "--libdir=" out "/lib")
 224                                        (string-append "--bindir=" out "/bin")
 225                                        (string-append "--pkgdir=" out)))))))))
 226     (home-page "https://github.com/ocaml/camlp4")
 227     (synopsis "Write parsers in OCaml")
 228     (description
 229      "Camlp4 is a software system for writing extensible parsers for
 230 programming languages.  It provides a set of OCaml libraries that are used to
 231 define grammars as well as loadable syntax extensions of such grammars.
 232 Camlp4 stands for Caml Preprocessor and Pretty-Printer and one of its most
 233 important applications is the definition of domain-specific extensions of the
 234 syntax of OCaml.")
 235
 236     ;; This is LGPLv2 with an exception that allows packages statically-linked
 237     ;; against the library to be released under any terms.
 238     (license lgpl2.0)))
 239
 240 (define-public camlp5
 241   (package
 242     (name "camlp5")
 243     (version "6.14")
 244     (source (origin
 245               (method url-fetch)
 246               (uri (string-append "http://camlp5.gforge.inria.fr/distrib/src/"
 247                                   name "-" version ".tgz"))
 248               (sha256
 249                (base32
 250                 "1ql04iyvclpyy9805kpddc4ndjb5d0qg4shhi2fc6bixi49fvy89"))))
 251     (build-system gnu-build-system)
 252     (inputs
 253      `(("ocaml" ,ocaml)))
 254     (arguments
 255      `(#:tests? #f  ; XXX TODO figure out how to run the tests
 256        #:phases
 257        (modify-phases %standard-phases
 258          (replace 'configure
 259                   (lambda* (#:key outputs #:allow-other-keys)
 260                     (let* ((out (assoc-ref outputs "out"))
 261                            (mandir (string-append out "/share/man")))
 262                       ;; Custom configure script doesn't recognize
 263                       ;; --prefix=<PREFIX> syntax (with equals sign).
 264                       (zero? (system* "./configure"
 265                                       "--prefix" out
 266                                       "--mandir" mandir)))))
 267          (replace 'build
 268                   (lambda _
 269                     (zero? (system* "make" "-j" (number->string
 270                                                  (parallel-job-count))
 271                                     "world.opt")))))))
 272     (home-page "http://camlp5.gforge.inria.fr/")
 273     (synopsis "Pre-processor Pretty Printer for OCaml")
 274     (description
 275      "Camlp5 is a Pre-Processor-Pretty-Printer for Objective Caml.  It offers
 276 tools for syntax (Stream Parsers and Grammars) and the ability to modify the
 277 concrete syntax of the language (Quotations, Syntax Extensions).")
 278     ;; Most files are distributed under bsd-3, but ocaml_stuff/* is under qpl.
 279     (license (list bsd-3 qpl))))
 280
 281 (define-public hevea
 282   (package
 283     (name "hevea")
 284     (version "2.23")
 285     (source (origin
 286               (method url-fetch)
 287               (uri (string-append "http://hevea.inria.fr/distri/"
 288                                   name "-" version ".tar.gz"))
 289               (sha256
 290                (base32
 291                 "1f9pj48518ixhjxbviv2zx27v4anp92zgg3x704g1s5cki2w33nv"))))
 292     (build-system gnu-build-system)
 293     (inputs
 294      `(("ocaml" ,ocaml)))
 295     (arguments
 296      `(#:tests? #f  ; no test suite
 297        #:make-flags (list (string-append "PREFIX=" %output))
 298        #:phases (modify-phases %standard-phases
 299                   (delete 'configure))))
 300     (home-page "http://hevea.inria.fr/")
 301     (synopsis "LaTeX to HTML translator")
 302     (description
 303      "HeVeA is a LaTeX to HTML translator that generates modern HTML 5.  It is
 304 written in Objective Caml.")
 305     (license qpl)))
 306
 307 (define-public coq
 308   (package
 309     (name "coq")
 310     (version "8.4pl6")
 311     (source (origin
 312               (method url-fetch)
 313               (uri (string-append "https://coq.inria.fr/distrib/V" version
 314                                   "/files/" name "-" version ".tar.gz"))
 315               (sha256
 316                (base32
 317                 "1mpbj4yf36kpjg2v2sln12i8dzqn8rag6fd07hslj2lpm4qs4h55"))))
 318     (build-system gnu-build-system)
 319     (native-inputs
 320      `(("texlive" ,texlive)
 321        ("hevea" ,hevea)))
 322     (inputs
 323      `(("ocaml" ,ocaml)
 324        ("camlp5" ,camlp5)))
 325     (arguments
 326      `(#:phases
 327        (modify-phases %standard-phases
 328          (replace 'configure
 329                   (lambda* (#:key outputs #:allow-other-keys)
 330                     (let* ((out (assoc-ref outputs "out"))
 331                            (mandir (string-append out "/share/man"))
 332                            (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
 333                       (zero? (system* "./configure"
 334                                       "--prefix" out
 335                                       "--mandir" mandir
 336                                       "--browser" browser)))))
 337          (replace 'build
 338                   (lambda _
 339                     (zero? (system* "make" "-j" (number->string
 340                                                  (parallel-job-count))
 341                                     "world"))))
 342          (delete 'check)
 343          (add-after 'install 'check
 344                     (lambda _
 345                       (with-directory-excursion "test-suite"
 346                         (zero? (system* "make"))))))))
 347     (home-page "https://coq.inria.fr")
 348     (synopsis "Proof assistant for higher-order logic")
 349     (description
 350      "Coq is a proof assistant for higher-order logic, which allows the
 351 development of computer programs consistent with their formal specification.
 352 It is developed using Objective Caml and Camlp5.")
 353     ;; The code is distributed under lgpl2.1.
 354     ;; Some of the documentation is distributed under opl1.0+.
 355     (license (list lgpl2.1 opl1.0+))))
 356
 357 (define-public proof-general
 358   (package
 359     (name "proof-general")
 360     (version "4.2")
 361     (source (origin
 362               (method url-fetch)
 363               (uri (string-append
 364                     "http://proofgeneral.inf.ed.ac.uk/releases/"
 365                     "ProofGeneral-" version ".tgz"))
 366               (sha256
 367                (base32
 368                 "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm"))))
 369     (build-system gnu-build-system)
 370     (native-inputs
 371      `(("which" ,which)
 372        ("emacs" ,emacs-no-x)
 373        ("texinfo" ,texinfo)))
 374     (inputs
 375      `(("host-emacs" ,emacs)
 376        ("perl" ,perl)
 377        ("coq" ,coq)))
 378     (arguments
 379      `(#:tests? #f  ; no check target
 380        #:make-flags (list (string-append "PREFIX=" %output)
 381                           (string-append "DEST_PREFIX=" %output))
 382        #:modules ((guix build gnu-build-system)
 383                   (guix build utils)
 384                   (guix build emacs-utils))
 385        #:imported-modules (,@%gnu-build-system-modules
 386                            (guix build emacs-utils))
 387        #:phases
 388        (modify-phases %standard-phases
 389          (delete 'configure)
 390          (add-after 'unpack 'disable-byte-compile-error-on-warn
 391                     (lambda _
 392                       (substitute* "Makefile"
 393                         (("\\(setq byte-compile-error-on-warn t\\)")
 394                          "(setq byte-compile-error-on-warn nil)"))
 395                       #t))
 396          (add-after 'unpack 'patch-hardcoded-paths
 397                     (lambda* (#:key inputs outputs #:allow-other-keys)
 398                       (let ((out   (assoc-ref outputs "out"))
 399                             (coq   (assoc-ref inputs "coq"))
 400                             (emacs (assoc-ref inputs "host-emacs")))
 401                         (define (coq-prog name)
 402                           (string-append coq "/bin/" name))
 403                         (emacs-substitute-variables "coq/coq.el"
 404                           ("coq-prog-name"           (coq-prog "coqtop"))
 405                           ("coq-compiler"            (coq-prog "coqc"))
 406                           ("coq-dependency-analyzer" (coq-prog "coqdep")))
 407                         (substitute* "Makefile"
 408                           (("/sbin/install-info") "install-info"))
 409                         (substitute* "bin/proofgeneral"
 410                           (("^PGHOMEDEFAULT=.*" all)
 411                            (string-append all
 412                                           "PGHOME=$PGHOMEDEFAULT\n"
 413                                           "EMACS=" emacs "/bin/emacs")))
 414                         #t)))
 415          (add-after 'unpack 'clean
 416                     (lambda _
 417                       ;; Delete the pre-compiled elc files for Emacs 23.
 418                       (zero? (system* "make" "clean"))))
 419          (add-after 'install 'install-doc
 420                     (lambda* (#:key make-flags #:allow-other-keys)
 421                       ;; XXX FIXME avoid building/installing pdf files,
 422                       ;; due to unresolved errors building them.
 423                       (substitute* "Makefile"
 424                         ((" [^ ]*\\.pdf") ""))
 425                       (zero? (apply system* "make" "install-doc"
 426                                     make-flags)))))))
 427     (home-page "http://proofgeneral.inf.ed.ac.uk/")
 428     (synopsis "Generic front-end for proof assistants based on Emacs")
 429     (description
 430      "Proof General is a major mode to turn Emacs into an interactive proof
 431 assistant to write formal mathematical proofs using a variety of theorem
 432 provers.")
 433     (license gpl2+)))
 434
 435 (define-public lablgtk
 436   (package
 437     (name "lablgtk")
 438     (version "2.18.3")
 439     (source
 440       (origin
 441         (method url-fetch)
 442           (uri (string-append "https://forge.ocamlcore.org/frs/download.php/"
 443                               "1479/lablgtk-2.18.3.tar.gz"))
 444           (sha256
 445             (base32
 446               "1bybn3jafxf4cx25zvn8h2xj9agn1xjbn7j3ywxxqx6az7rfnnwp"))))
 447     (build-system gnu-build-system)
 448     (native-inputs
 449      `(("camlp4" ,camlp4)
 450        ("ocaml" ,ocaml)
 451        ("pkg-config" ,pkg-config)))
 452     ;; FIXME: Add inputs gtkgl-2.0, libpanelapplet-2.0, gtkspell-2.0,
 453     ;; and gtk+-quartz-2.0 once available.
 454     (inputs
 455      `(("gtk+" ,gtk+-2)
 456        ("gtksourceview" ,gtksourceview)
 457        ("libgnomecanvas" ,libgnomecanvas)
 458        ("libgnomeui" ,libgnomeui)
 459        ("libglade" ,libglade)
 460        ("librsvg" ,librsvg)))
 461     (arguments
 462      `(#:tests? #f ; no check target
 463
 464        ;; Occasionally we would get "Error: Unbound module GtkThread" when
 465        ;; compiling 'gtkThInit.ml', with 'make -j'.  So build sequentially.
 466        #:parallel-build? #f
 467
 468        #:phases
 469          (modify-phases %standard-phases
 470            (replace 'install
 471              (lambda* (#:key inputs outputs #:allow-other-keys)
 472                (let ((out (assoc-ref outputs "out"))
 473                      (ocaml (assoc-ref inputs "ocaml")))
 474                  ;; Install into the output and not the ocaml directory.
 475                  (substitute* "config.make"
 476                    ((ocaml) out))
 477                  (system* "make" "old-install")
 478                  #t))))))
 479     (home-page "http://lablgtk.forge.ocamlcore.org/")
 480     (synopsis "GTK+ bindings for OCaml")
 481     (description
 482      "LablGtk is an OCaml interface to GTK+ 1.2 and 2.x.  It provides
 483 a strongly-typed object-oriented interface that is compatible with the
 484 dynamic typing of GTK+.  Most widgets and methods are available.  LablGtk
 485 also provides bindings to
 486 gdk-pixbuf, the GLArea widget (in combination with LablGL), gnomecanvas,
 487 gnomeui, gtksourceview, gtkspell,
 488 libglade (and it an generate OCaml code from .glade files),
 489 libpanel, librsvg and quartz.")
 490     (license lgpl2.1)))
 491
 492 (define-public unison
 493   (package
 494     (name "unison")
 495     (version "2.48.3")
 496     (source
 497       (origin
 498         (method url-fetch)
 499           (uri (string-append "https://www.seas.upenn.edu/~bcpierce/unison/"
 500                               "download/releases/stable/unison-" version
 501                               ".tar.gz"))
 502           (sha256
 503             (base32
 504               "10sln52rnnsj213jy3166m0q97qpwnrwl6mm529xfy10x3xkq3gl"))))
 505     (build-system gnu-build-system)
 506     (native-inputs
 507      `(("ocaml" ,ocaml)))
 508     (arguments
 509      `(#:parallel-build? #f
 510        #:parallel-tests? #f
 511        #:test-target "selftest"
 512        #:tests? #f ; Tests require writing to $HOME.
 513                    ; If some $HOME is provided, they fail with the message
 514                    ; "Fatal error: Skipping some tests -- remove me!"
 515        #:phases
 516          (modify-phases %standard-phases
 517            (delete 'configure)
 518            (add-before 'install 'prepare-install
 519              (lambda* (#:key outputs #:allow-other-keys)
 520                (let* ((out (assoc-ref outputs "out"))
 521                       (bin (string-append out "/bin")))
 522                  (mkdir-p bin)
 523                  (setenv "HOME" out) ; forces correct INSTALLDIR in Makefile
 524                  #t))))))
 525     (home-page "https://www.cis.upenn.edu/~bcpierce/unison/")
 526     (synopsis "File synchronizer")
 527     (description
 528      "Unison is a file-synchronization tool.  It allows two replicas of
 529 a collection of files and directories to be stored on different hosts
 530 (or different disks on the same host), modified separately, and then
 531 brought up to date by propagating the changes in each replica
 532 to the other.")
 533     (license gpl3+)))