diff options
| author | Julien Lepiller <julien@lepiller.eu> | 2017-10-21 18:05:11 +0200 |
|---|---|---|
| committer | Julien Lepiller <julien@lepiller.eu> | 2017-10-22 10:21:22 +0200 |
| commit | dbfb1a596ae75554fd9bc3f9ff5024789e790091 (patch) | |
| tree | be8661f692222accb6600859d8d8328029e09bc7 /gnu | |
| parent | 3ffd180cc5284f8ee3c61073593347fbb042fe58 (diff) | |
| download | guix-dbfb1a596ae75554fd9bc3f9ff5024789e790091.tar.gz | |
gnu: Add coq-bignums.
* gnu/packages/ocaml.scm (coq-bignums): New variable.
Diffstat (limited to 'gnu')
| -rw-r--r-- | gnu/packages/ocaml.scm | 32 |
1 files changed, 32 insertions, 0 deletions
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") |