Merge branch 'master' into core-updates

1 files changed, 91 insertions, 3 deletions

diff --git a/gnu/packages/algebra.scm b/gnu/packages/algebra.scm
index 7c64f4461e..6e7ecdad05 100644
--- a/gnu/packages/algebra.scm
+++ b/gnu/packages/algebra.scm
@@ -7,7 +7,7 @@
 ;;; Copyright © 2017, 2020, 2021 Efraim Flashner <efraim@flashner.co.il>
 ;;; Copyright © 2017–2021 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;; Copyright © 2017 Marius Bakke <mbakke@fastmail.com>
-;;; Copyright © 2017, 2019 Eric Bavier <bavier@member.fsf.org>
+;;; Copyright © 2017, 2019, 2021 Eric Bavier <bavier@posteo.net>
 ;;; Copyright © 2019 Mathieu Othacehe <m.othacehe@gmail.com>
 ;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de>
 ;;; Copyright © 2020 Jakub Kądziołka <kuba@kadziolka.net>
@@ -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)
@@ -59,6 +60,7 @@
   #:use-module (gnu packages tex)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages xiph)
+  #:use-module (gnu packages xml)
   #:use-module (gnu packages xorg)
   #:use-module (guix build-system ant)
   #:use-module (guix build-system gnu)
@@ -341,7 +343,7 @@ precision.")
 (define-public giac
   (package
     (name "giac")
-    (version "1.7.0-13")
+    (version "1.7.0-17")
     (source
      (origin
        (method url-fetch)
@@ -353,7 +355,7 @@ precision.")
                            "~parisse/debian/dists/stable/main/source/"
                            "giac_" version ".tar.gz"))
        (sha256
-        (base32 "14ywcnk7q27fpd7cr3wixhnd51qb2h2wl2kj6zs6bw2yi6dharfk"))))
+        (base32 "0yh556wlgs9hfyp5j2xz4nlrd2dma63cicrc3dhahyl96y1aw6mr"))))
     (build-system gnu-build-system)
     (arguments
      `(#:modules ((ice-9 ftw)
@@ -1246,6 +1248,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")
@@ -1609,3 +1652,48 @@ no more than about 20 bits long).")
 (@dfn{DCT}), Discrete Sine Transform (@dfn{DST}) and Discrete Hartley Transform
 (@dfn{DHT}).")
     (license license:gpl2+)))
+
+(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 license:cecill-c)))