From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:55819) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1e5wYG-0007xo-7D for guix-patches@gnu.org; Sat, 21 Oct 2017 12:23:09 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1e5wYF-0002my-5f for guix-patches@gnu.org; Sat, 21 Oct 2017 12:23:08 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:45823) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1e5wYF-0002mt-2c for guix-patches@gnu.org; Sat, 21 Oct 2017 12:23:07 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1e5wYE-000339-RY for guix-patches@gnu.org; Sat, 21 Oct 2017 12:23:06 -0400 Subject: [bug#28925] [PATCH 6/7] gnu: Add coq-bignums. Resent-Message-ID: From: julien@lepiller.eu Date: Sat, 21 Oct 2017 18:20:57 +0200 Message-Id: <20171021162058.27938-7-julien@lepiller.eu> In-Reply-To: <20171021162058.27938-1-julien@lepiller.eu> References: <20171021181638.27d0d0d8@lepiller.eu> <20171021162058.27938-1-julien@lepiller.eu> List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 28925@debbugs.gnu.org From: Julien Lepiller * gnu/packages/ocaml.scm (coq-bignums): New variable. --- gnu/packages/ocaml.scm | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 6cf92689a..addcdba5a 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3746,6 +3746,38 @@ conservative extension of Coq's standard library and provides correspondence theorems between the two libraries.") (license license:lgpl3+))) +(define-public coq-bignums + (package + (name "coq-bignums") + (version "8.7.0") + (source (origin + (method url-fetch) + (uri (string-append "https://github.com/coq/bignums/archive/V" + version ".tar.gz")) + (file-name (string-append name "-" version ".tar.gz")) + (sha256 + (base32 + "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("coq" ,coq))) + (inputs + `(("camlp5" ,camlp5))) + (arguments + `(#:tests? #f; No test target + #:make-flags + (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) + #:phases + (modify-phases %standard-phases + (delete 'configure)))) + (home-page "https://github.com/coq/bignums") + (synopsis "Coq library for arbitrary large numbers") + (description "Bignums is a coq library of arbitrary large numbers. It +provides BigN, BigZ, BigQ that used to be part of Coq standard library.") + (license license:lgpl2.1+))) + (define-public coq-interval (package (name "coq-interval") -- 2.14.2