From mboxrd@z Thu Jan 1 00:00:00 1970 From: Nikita Karetnikov Subject: Packaging Coq Date: Thu, 04 Dec 2014 05:02:27 +0400 Message-ID: <87ppc0447w.fsf@karetnikov.org> Mime-Version: 1.0 Content-Type: multipart/signed; boundary="==-=-="; micalg=pgp-sha1; protocol="application/pgp-signature" Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:55360) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XwLl2-0004cJ-Rv for guix-devel@gnu.org; Wed, 03 Dec 2014 21:03:08 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1XwLky-0007Hq-Nz for guix-devel@gnu.org; Wed, 03 Dec 2014 21:03:04 -0500 Received: from li305-5.members.linode.com ([178.79.168.5]:37266 helo=cooksoni.karetnikov.org) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1XwLky-0007Gh-F6 for guix-devel@gnu.org; Wed, 03 Dec 2014 21:03:00 -0500 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: multipart/mixed; boundary="=-=-=" --=-=-= Does anyone know how to proceed? --=-=-= Content-Type: text/plain; charset=utf-8 Content-Disposition: attachment; filename=coq.scm Content-Transfer-Encoding: quoted-printable ;;; GNU Guix --- Functional package management for GNU ;;; Copyright =C2=A9 2014 Nikita Karetnikov ;;; ;;; 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 . (define-module (gnu packages coq) #:use-module (guix licenses) #:use-module (guix packages) #:use-module (guix download) #:use-module (guix build-system gnu) #:use-module (gnu packages compression) #:use-module (gnu packages ocaml)) (define-public coq (package (name "coq") (version "8.4pl5") (source (origin (method url-fetch) (uri (string-append "https://" name ".inria.fr/distrib/V" version "/files/" name "-" version ".tar.gz")) (sha256 (base32 "0iajsabyrgypk1ncm0kqcxqv02k24xa1bayaxacjgmsqiavmm09m")))) (build-system gnu-build-system) (arguments '(#:phases (alist-replace 'configure (lambda* (#:key outputs #:allow-other-keys) ;; This 'configure' script doesn't support ;; variables passed as arguments. (let ((out (assoc-ref outputs "out"))) (setenv "CONFIG_SHELL" (which "bash")) (zero? ;; 'configure' does not recognize the flags if y= ou ;; use 'system*'. (system (string-append "./configure" " -prefix " out " -camldir " (dirname (which "ocaml"))= ))))) (alist-replace 'build (lambda _ (system* "make" "world")) (alist-replace 'check (lambda _ (chdir "test-suite") (system* "make" "chec= k") (chdir "..")) %standard-phases))))) (native-inputs `(("ocaml" ,ocaml) ("bzip2" ,bzip2))) (home-page "https://coq.inria.fr") (synopsis "Formal proof management system") (description "Coq is a formal proof management system. It provides a formal langua= ge to write mathematical definitions, executable algorithms and theorems toget= her with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages, the formalization of mathematics (e.g., the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.") (license lgpl2.1))) --=-=-=-- --==-=-= Content-Type: application/pgp-signature -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) iQIcBAEBAgAGBQJUf7KoAAoJEM+IQzI9IQ38jtAP/0Xdo0EEO+6qR2TXxzSgglbF 8g/ziznpN9BfSHhSNWYZBdftZ/XodSPRrcgybEqE4KEQXU6q8ntpP1LX7MWIO1fG eRHz/xxodv7khkS1PkTfekTFyykRJAPjYnaokh0a4VoLNRwhZV4RHi3/XFQ9Rvnp UEAdv9OcQ7h7v+kPHZQMQn0HWSsR9JhQ04FuuXR0Mysiz2Pq6MvEcT5B5ZpmKvlB P4gfjQ9G/ZJiGfo3nCHOy0nL3WHCl1cPpJNlLDfIf/zPlXUlUQPQJPJHSGZRdX7M dvq4YJwpcYIcOr5fC4B4fwz5UPZeOJ7rNjIncQ2eUBS30O/uQDZrhB9jT5kCly/x NxVvk6t4MXEsDJGe4X0duJMrCmEy6GU5M/h//XqWLdwt5JZyAKlcevB5kO/EDni9 3lLogf1Wc2orB1nOkmk375MVNIab7jV1K+PWt9lH40NWWZ7h9DuvdEXID6zy8SqL sEnBDiUjQLv2kTXoYHvRYVDZJeJ+MVljmumOowMUNXz0iC3h48SPV0nwtE1dl34N FNfrdB0SrOcTZsqH5ZmUJajLuPh274V9c+SLEE7hPPU1xQHLXiUl7Xh+i3G5AoL8 5NaQdX4lCxF+p9YWwL5wXJQfKEGeZjIgjWmZXsOoeu0yRICKCOXvOtwF6mgmQ9m3 DVTaYhIlJNAn06Pp6Rv1 =MiOj -----END PGP SIGNATURE----- --==-=-=--