From dbfb1a596ae75554fd9bc3f9ff5024789e790091 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sat, 21 Oct 2017 18:05:11 +0200 Subject: gnu: Add coq-bignums. * 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 6cf92689ac..addcdba5a0 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") -- cgit v1.2.3