GNU bug report logs - #28925
[PATCH] Update coq and coq libraries.

Previous Next

Full log

Message #29 received at 28925 <at> debbugs.gnu.org (full text, mbox):

From: julien <at> lepiller.eu
To: 28925 <at> debbugs.gnu.org
Cc: Julien Lepiller <julien <at> lepiller.eu>
Subject: [PATCH 6/7] gnu: Add coq-bignums.
Date: Sat, 21 Oct 2017 18:20:57 +0200

From: Julien Lepiller <julien <at> lepiller.eu>

* 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.