Does anyone know how to proceed?
;;; GNU Guix --- Functional package management for GNU ;;; Copyright © 2014 Nikita Karetnikov <nik...@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)))
pgpp5l7n4cgnM.pgp
Description: PGP signature
