[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
04/05: gnu: Add coq-coquelicot.
From: |
julien lepiller |
Subject: |
04/05: gnu: Add coq-coquelicot. |
Date: |
Sat, 29 Jul 2017 09:20:16 -0400 (EDT) |
roptat pushed a commit to branch master
in repository guix.
commit b09c4244f7c77b11e039cd5348270b2d1da77577
Author: Julien Lepiller <address@hidden>
Date: Wed Jun 21 21:40:23 2017 +0200
gnu: Add coq-coquelicot.
* gnu/packages/ocaml.scm (coq-coquelicot): New variable.
---
gnu/packages/ocaml.scm | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 50 insertions(+)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 1ed0ffa..86af187 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3295,3 +3295,53 @@ of the Odd Order Theorem.
The library is written using the Ssreflect proof language that is an integral
part of the distribution.")
(license license:cecill-b)))
+
+(define-public coq-coquelicot
+ (package
+ (name "coq-coquelicot")
+ (version "3.0.0")
+ (source (origin
+ (method url-fetch)
+ (uri (string-append "https://gforge.inria.fr/frs/download.php/"
+ "file/36537/coquelicot-" version ".tar.gz"))
+ (sha256
+ (base32
+ "0fx99bvsbdizj00gx2im8939y4wwl05f4qhw184j90kcx5vjxxv9"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("ocaml" ,ocaml)
+ ("which" ,which)
+ ("coq" ,coq)))
+ (propagated-inputs
+ `(("mathcomp" ,coq-mathcomp)))
+ (arguments
+ `(#:configure-flags
+ (list (string-append "--libdir=" (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib/Coquelicot"))
+ #: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"))))
+ (replace 'install
+ (lambda _
+ (zero? (system* "./remake" "install")))))))
+ (home-page "http://coquelicot.saclay.inria.fr/index.html")
+ (synopsis "Coq library for Reals")
+ (description "Coquelicot is an easier way of writing formulas and theorem
+statements, achieved by relying on total functions in place of dependent types
+for limits, derivatives, integrals, power series, and so on. To help with the
+proof process, the library comes with a comprehensive set of theorems that
cover
+not only these notions, but also some extensions such as parametric integrals,
+two-dimensional differentiability, asymptotic behaviors. It also offers some
+automations for performing differentiability proofs. Moreover, Coquelicot is a
+conservative extension of Coq's standard library and provides correspondence
+theorems between the two libraries.")
+ (license license:lgpl3+)))