summaryrefslogtreecommitdiff
path: root/gnu
diff options
context:
space:
mode:
authorEric Bavier <bavier@posteo.net>2021-06-23 22:28:05 -0500
committerEric Bavier <bavier@posteo.net>2021-06-23 22:29:24 -0500
commitd320daf7df3f5a50447158c1244bdc4fa57973ac (patch)
tree962e23d7c07772c5b294231c24aca511e5de8e26 /gnu
parent6d388103a4ed8f14f1ac6ac7a2ff22c5fa6b8cd4 (diff)
gnu: Add Gappa.
* gnu/packages/algebra.scm (gappa): New variable.
Diffstat (limited to 'gnu')
-rw-r--r--gnu/packages/algebra.scm42
1 files changed, 42 insertions, 0 deletions
diff --git a/gnu/packages/algebra.scm b/gnu/packages/algebra.scm
index 5227d6797b..34a9bd202c 100644
--- a/gnu/packages/algebra.scm
+++ b/gnu/packages/algebra.scm
@@ -34,6 +34,7 @@
#:use-module (gnu packages)
#:use-module (gnu packages autotools)
#:use-module (gnu packages bison)
+ #:use-module (gnu packages boost)
#:use-module (gnu packages check)
#:use-module (gnu packages compression)
#:use-module (gnu packages cpp)
@@ -1245,6 +1246,47 @@ objects.")
;; safe side, we drop them for now.
(license license:gpl2+)))
+(define-public gappa
+ (package
+ (name "gappa")
+ (version "1.3.5")
+ (source (origin
+ (method url-fetch)
+ (uri (string-append "https://gforge.inria.fr/frs/download.php/latestfile/"
+ "2699/gappa-" version ".tar.gz"))
+ (sha256
+ (base32
+ "0q1wdiwqj6fsbifaayb1zkp20bz8a1my81sqjsail577jmzwi07w"))))
+ (build-system gnu-build-system)
+ (inputs
+ `(("boost" ,boost)
+ ("gmp" ,gmp)
+ ("mpfr" ,mpfr)))
+ (arguments
+ `(#:phases
+ (modify-phases %standard-phases
+ (add-after 'unpack 'patch-remake-shell
+ (lambda _
+ (substitute* "remake.cpp"
+ (("/bin/sh") (which "sh")))
+ #t))
+ (replace 'build
+ (lambda _ (invoke "./remake" "-s" "-d")))
+ (replace 'install
+ (lambda _ (invoke "./remake" "-s" "-d" "install")))
+ (replace 'check
+ (lambda _ (invoke "./remake" "check"))))))
+ (home-page "http://gappa.gforge.inria.fr/")
+ (synopsis "Proof generator for arithmetic properties")
+ (description "Gappa is a tool intended to help verifying and formally
+proving properties on numerical programs dealing with floating-point or
+fixed-point arithmetic. It has been used to write robust floating-point
+filters for CGAL and it is used to certify elementary functions in CRlibm.
+While Gappa is intended to be used directly, it can also act as a backend
+prover for the Why3 software verification platform or as an automatic tactic
+for the Coq proof assistant.")
+ (license (list license:gpl3+ license:cecill-c)))) ; either/or
+
(define-public givaro
(package
(name "givaro")