|
|
@@ -1,99 +0,0 @@
|
|
|
-;;; 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://www.sollya.org/releases/"
|
|
|
- "sollya-" version "/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
|
|
|
- `(#:configure-flags (list (string-append "--docdir=${datadir}/doc/sollya-" ,version))
|
|
|
- #: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 "https://www.sollya.org")
|
|
|
- (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/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 gpl3+ cecill-c)))) ; either/or
|
Eric Bavier