From: Nikita Karetnikov <nikita@karetnikov.org>
To: guix-devel@gnu.org
Subject: Packaging Coq
Date: Thu, 04 Dec 2014 05:02:27 +0400 [thread overview]
Message-ID: <87ppc0447w.fsf@karetnikov.org> (raw)
[-- Attachment #1.1: Type: text/plain, Size: 34 bytes --]
Does anyone know how to proceed?
[-- Attachment #1.2: coq.scm --]
[-- Type: text/plain, Size: 3563 bytes --]
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2014 Nikita Karetnikov <nikita@karetnikov.org>
;;;
;;; 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 (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 you
;; 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" "check")
(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 language
to write mathematical definitions, executable algorithms and theorems together
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)))
[-- Attachment #2: Type: application/pgp-signature, Size: 835 bytes --]
next reply other threads:[~2014-12-04 2:03 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-12-04 1:02 Nikita Karetnikov [this message]
2014-12-04 9:49 ` Packaging Coq Nikita Karetnikov
2014-12-04 10:26 ` Nikita Karetnikov
2014-12-04 10:07 ` Andreas Enge
2014-12-04 18:35 ` Ludovic Courtès
2014-12-04 23:56 ` Mark H Weaver
2014-12-05 11:17 ` Andreas Enge
2014-12-05 14:59 ` Mark H Weaver
2014-12-05 15:52 ` Andreas Enge
2014-12-05 19:03 ` Ludovic Courtès
2014-12-04 10:34 ` John Darrington
2014-12-04 9:46 ` Nikita Karetnikov
2014-12-05 5:25 ` Mark H Weaver
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=87ppc0447w.fsf@karetnikov.org \
--to=nikita@karetnikov.org \
--cc=guix-devel@gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.