|
|
@@ -0,0 +1,98 @@
|
|
|
+;;; This file is part of guix-bavier.git
|
|
|
+;;; Copyright © 2020 Eric Bavier <bavier@posteo.net>
|
|
|
+;;; License: GPLv3+
|
|
|
+
|
|
|
+(define-module (bavier packages algebra)
|
|
|
+ #:use-module (guix build-system gnu)
|
|
|
+ #:use-module (guix download)
|
|
|
+ #:use-module (guix licenses)
|
|
|
+ #:use-module (guix packages)
|
|
|
+ #:use-module (gnu packages algebra)
|
|
|
+ #:use-module (gnu packages boost)
|
|
|
+ #:use-module (gnu packages maths)
|
|
|
+ #:use-module (gnu packages multiprecision)
|
|
|
+ #:use-module (gnu packages xml))
|
|
|
+
|
|
|
+(define-public sollya
|
|
|
+ (package
|
|
|
+ (name "sollya")
|
|
|
+ (version "7.0")
|
|
|
+ (source (origin
|
|
|
+ (method url-fetch)
|
|
|
+ (uri (string-append "https://gforge.inria.fr/frs/download.php/file/"
|
|
|
+ "37748/sollya-" version ".tar.bz2"))
|
|
|
+ (sha256
|
|
|
+ (base32
|
|
|
+ "11290ivi9h665cxi8f1shlavhy10vzb8s28m57hrcgnxyxqmhx0m"))))
|
|
|
+ (build-system gnu-build-system)
|
|
|
+ (inputs
|
|
|
+ `(("fplll" ,fplll)
|
|
|
+ ("gmp" ,gmp)
|
|
|
+ ("gnuplot" ,gnuplot)
|
|
|
+ ("libxml2" ,libxml2)
|
|
|
+ ("mpfi" ,mpfi)
|
|
|
+ ("mpfr" ,mpfr)))
|
|
|
+ (arguments
|
|
|
+ `(#:phases
|
|
|
+ (modify-phases %standard-phases
|
|
|
+ (add-after 'unpack 'patch-test-shebang
|
|
|
+ (lambda _
|
|
|
+ (substitute* (list "tests-tool/Makefile.in"
|
|
|
+ "tests-lib/Makefile.in")
|
|
|
+ (("#!/bin/sh") (string-append "#!" (which "sh"))))
|
|
|
+ #t))
|
|
|
+ (add-before 'build 'patch-gnuplot-reference
|
|
|
+ (lambda _
|
|
|
+ (substitute* "general.c"
|
|
|
+ (("\"gnuplot\"") (string-append "\"" (which "gnuplot") "\"")))
|
|
|
+ #t)))))
|
|
|
+ (home-page "http://sollya.gforge.inria.fr/")
|
|
|
+ (synopsis "Development environment for safe floating-point code")
|
|
|
+ (description "Sollya is a computer program whose purpose is to
|
|
|
+provide an environment for safe floating-point code development. It
|
|
|
+is particularly targeted to the automated implementation of
|
|
|
+mathematical floating-point libraries (libm). Amongst other features,
|
|
|
+it offers a certified infinity norm, an automatic polynomial
|
|
|
+implementer, and a fast Remez algorithm.")
|
|
|
+ (license cecill-c)))
|
|
|
+
|
|
|
+(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/file/"
|
|
|
+ "38044/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 gpl3+ cecill-c)))) ; either/or
|
Eric Bavier