From mboxrd@z Thu Jan 1 00:00:00 1970 From: Mark H Weaver Subject: [PATCHES] gnu: Update ocaml; Add camlp5, hevea, and coq. Date: Wed, 03 Jun 2015 04:56:49 -0400 Message-ID: <87k2vlqiem.fsf@netris.org> Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:43240) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Z04UB-0002D8-Ar for guix-devel@gnu.org; Wed, 03 Jun 2015 04:57:21 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1Z04U7-00036p-RP for guix-devel@gnu.org; Wed, 03 Jun 2015 04:57:19 -0400 Received: from world.peace.net ([50.252.239.5]:48367) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Z04U7-0002kg-KW for guix-devel@gnu.org; Wed, 03 Jun 2015 04:57:15 -0400 List-Id: "Development of GNU Guix and the GNU System distribution." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org Sender: guix-devel-bounces+gcggd-guix-devel=m.gmane.org@gnu.org To: guix-devel@gnu.org --=-=-= Content-Type: text/plain These patches update and improve our ocaml package, and add packages for camlp5, hevea, and coq. They also add the Open Publication License 1.0 or later. Mark --=-=-= Content-Type: text/x-patch; charset=utf-8 Content-Disposition: inline; filename=0001-gnu-ocaml-Update-to-4.02.1.patch Content-Transfer-Encoding: quoted-printable Content-Description: [PATCH 1/5] gnu: ocaml: Update to 4.02.1 >From f2b8ab36b2d3697b7a93b87bfcbcd0e91294c2e1 Mon Sep 17 00:00:00 2001 From: Mark H Weaver Date: Tue, 2 Jun 2015 22:49:10 -0400 Subject: [PATCH 1/5] gnu: ocaml: Update to 4.02.1. * gnu/packages/ocaml.scm (ocaml)[version]: Update to 4.02.1. [source]: Use 'version-major+minor'. Use .xz tarball. [home-page]: Update URI. [license]: gpl2 -> lgpl2.0. [inputs]: Add libx11, gcc:lib, and zlib. Remove perl. [native-inputs]: New field, with perl and pkg-config. [arguments]: In #:modules, remove (srfi srfi-1), add (web server). Use 'modify-phases'. Enable parallel build. Add 'patch-/bin/sh-references' = and 'prepare-socket-test' phases. Rename 'check-after-install' phase to 'check'. Use 'with-directory-excursion' in 'check' phase. Remove unused keyword arguments from custom phases. --- gnu/packages/ocaml.scm | 129 ++++++++++++++++++++++++++++++++-------------= ---- 1 file changed, 86 insertions(+), 43 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 2b4821e..a076078 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -1,6 +1,6 @@ ;;; GNU Guix --- Functional package management for GNU ;;; Copyright =C2=A9 2013 Cyril Roelandt -;;; Copyright =C2=A9 2014 Mark H Weaver +;;; Copyright =C2=A9 2014, 2015 Mark H Weaver ;;; ;;; This file is part of GNU Guix. ;;; @@ -18,11 +18,16 @@ ;;; along with GNU Guix. If not, see . =20 (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 pkg-config) + #:use-module (gnu packages compression) + #:use-module (gnu packages commencement) + #:use-module (gnu packages xorg) #:use-module (gnu packages perl) #:use-module (gnu packages python) #:use-module (gnu packages ncurses) @@ -32,56 +37,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 su= pport + ("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 " rather than the usual - ;; "--prefix=3D". - (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" ta= rget. - (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=3D 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 808= 0~%") + (when (zero? (primitive-fork)) + (run-server (lambda (request request-body) + (values '((content-type . (text/pla= in))) + "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 year= s 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)))) =20 (define-public opam (package --=20 2.2.1 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0002-gnu-Add-camlp5.patch Content-Description: [PATCH 2/5] gnu: Add camlp5 >From b9d2f69ef9b51fc8b987fe703e507bf3603b875a Mon Sep 17 00:00:00 2001 From: Mark H Weaver Date: Sat, 30 May 2015 14:59:54 -0400 Subject: [PATCH 2/5] gnu: Add camlp5. * gnu/packages/ocaml.scm (camlp5): New variable. --- gnu/packages/ocaml.scm | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index a076078..5407670 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -186,3 +186,42 @@ 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"))) + (zero? (system* + "./configure" + "--prefix" out + "--mandir" (string-append out "/share/man")))))) + (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)))) -- 2.2.1 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0003-gnu-Add-hevea.patch Content-Description: [PATCH 3/5] gnu: Add hevea >From fb9fd9480762be66796df53e756b430551b88d3c Mon Sep 17 00:00:00 2001 From: Mark H Weaver Date: Wed, 3 Jun 2015 03:21:43 -0400 Subject: [PATCH 3/5] gnu: Add hevea. * gnu/packages/ocaml.scm (hevea): New variable. --- gnu/packages/ocaml.scm | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 5407670..7449455 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -225,3 +225,29 @@ 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))) -- 2.2.1 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0004-licenses-Add-the-Open-Publication-License-1.0.patch Content-Description: [PATCH 4/5] licenses: Add the Open Publication License 1.0 >From f2ab73018cbaec826472dc0c162e5440fe00bcd9 Mon Sep 17 00:00:00 2001 From: Mark H Weaver Date: Wed, 3 Jun 2015 01:18:26 -0400 Subject: [PATCH 4/5] licenses: Add the Open Publication License 1.0. * guix/licenses.scm (opl1.0+): New variable. --- guix/licenses.scm | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/guix/licenses.scm b/guix/licenses.scm index 1be3500..4804421 100644 --- a/guix/licenses.scm +++ b/guix/licenses.scm @@ -37,6 +37,7 @@ freetype gpl1 gpl1+ gpl2 gpl2+ gpl3 gpl3+ fdl1.3+ + opl1.0+ isc ijg ibmpl1.0 @@ -206,6 +207,11 @@ at URI, which may be a file:// URI pointing the package's tree." "https://www.gnu.org/licenses/fdl.html" "https://www.gnu.org/licenses/license-list#FDL")) +(define opl1.0+ + (license "Open Publication License 1.0 or later" + "http://opencontent.org/openpub/" + "https://www.gnu.org/licenses/license-list#OpenPublicationL")) + (define isc (license "ISC" "http://directory.fsf.org/wiki/License:ISC" -- 2.2.1 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0005-gnu-Add-coq.patch Content-Description: [PATCH 5/5] gnu: Add coq >From deb7f49fdce90f546b4fd0ee50290aa61c854ef0 Mon Sep 17 00:00:00 2001 From: Mark H Weaver Date: Sat, 30 May 2015 16:07:19 -0400 Subject: [PATCH 5/5] gnu: Add coq. * gnu/packages/ocaml.scm (coq): New variable. --- gnu/packages/ocaml.scm | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 7449455..a63acdc 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -28,6 +28,7 @@ #: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) @@ -251,3 +252,53 @@ concrete syntax of the language (Quotations, Syntax Extensions).") "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"))) + (zero? (system* + "./configure" + "--prefix" out + "--mandir" (string-append out "/share/man") + "--browser" + "icecat -remote \"OpenURL(%s,new-tab)\""))))) + (replace 'build + (lambda _ + (zero? (system* "make" + "-j" (number->string (parallel-job-count)) + "world")))) + (delete 'check) + (add-after 'install 'check-after-install + (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+)))) -- 2.2.1 --=-=-=--