diff options
| author | Julien Lepiller <julien@lepiller.eu> | 2017-06-08 18:25:32 +0200 |
|---|---|---|
| committer | Julien Lepiller <julien@lepiller.eu> | 2017-07-29 15:18:45 +0200 |
| commit | d163d97d92f3abea98f4b36d55ac3bb9db23d423 (patch) | |
| tree | 29fd3747c19f550dbed61ace9522756ba27506ac /gnu/packages | |
| parent | 8f82110492c0ecdb2fe0f6aba0a981cb34c66472 (diff) | |
gnu: Add coq-flocq.
* gnu/packages/ocaml.scm (coq-flocq): New variable.
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/ocaml.scm | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 68619019f1..82da0bf1d0 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3153,3 +3153,48 @@ writing to these structures, and they are accessed via the Bigarray module.") (synopsis "Minimal library providing hexadecimal converters") (description "Hex is a minimal library providing hexadecimal converters.") (license license:isc))) + +(define-public coq-flocq + (package + (name "coq-flocq") + (version "2.5.2") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/file" + "/36199/flocq-" version ".tar.gz")) + (sha256 + (base32 + "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Flocq")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))))) + (replace 'build + (lambda _ + (zero? (system* "./remake")))) + (replace 'check + (lambda _ + (zero? (system* "./remake" "check")))) + ;; TODO: requires coq-gappa and coq-interval. + ;(zero? (system* "./remake" "check-more")))) + (replace 'install + (lambda _ + (zero? (system* "./remake" "install"))))))) + (home-page "http://flocq.gforge.inria.fr/") + (synopsis "Floating-point formalization for the Coq system") + (description "Flocq (Floats for Coq) is a floating-point formalization for +the Coq system. It provides a comprehensive library of theorems on a multi-radix +multi-precision arithmetic. It also supports efficient numerical computations +inside Coq.") + (license license:lgpl3+))) |