gnu: libqalculate: Update to 3.19.0.
[jackhill/guix/guix.git] / gnu / packages / maths.scm
index 3991b2f..f665897 100644 (file)
@@ -2,17 +2,17 @@
 ;;; Copyright © 2013, 2014, 2015, 2016, 2019, 2020 Andreas Enge <andreas@enge.fr>
 ;;; Copyright © 2013 Nikita Karetnikov <nikita@karetnikov.org>
 ;;; Copyright © 2014, 2016, 2017 John Darrington <jmd@gnu.org>
-;;; Copyright © 2014, 2015, 2016, 2017, 2018, 2019, 2020 Eric Bavier <bavier@posteo.net>
+;;; Copyright © 2014, 2015, 2016, 2017, 2018, 2019, 2020, 2021 Eric Bavier <bavier@posteo.net>
 ;;; Copyright © 2014 Federico Beffa <beffa@fbengineering.ch>
 ;;; Copyright © 2014 Mathieu Lirzin <mathieu.lirzin@openmailbox.org>
 ;;; Copyright © 2015, 2016, 2017, 2018, 2019, 2020 Ricardo Wurmus <rekado@elephly.net>
 ;;; Copyright © 2015 Sou Bunnbu <iyzsong@gmail.com>
 ;;; Copyright © 2015, 2018 Mark H Weaver <mhw@netris.org>
-;;; Copyright © 2015, 2016, 2017, 2018, 2019, 2020 Efraim Flashner <efraim@flashner.co.il>
+;;; Copyright © 2015, 2016, 2017, 2018, 2019, 2020, 2021 Efraim Flashner <efraim@flashner.co.il>
 ;;; Copyright © 2015 Fabian Harfert <fhmgufs@web.de>
 ;;; Copyright © 2016 Roel Janssen <roel@gnu.org>
 ;;; Copyright © 2016, 2018, 2020 Kei Kebreau <kkebreau@posteo.net>
-;;; Copyright © 2016, 2017, 2018, 2019, 2020 Ludovic Courtès <ludo@gnu.org>
+;;; Copyright © 2016, 2017, 2018, 2019, 2020, 2021 Ludovic Courtès <ludo@gnu.org>
 ;;; Copyright © 2016 Leo Famulari <leo@famulari.name>
 ;;; Copyright © 2016, 2017 Thomas Danckaert <post@thomasdanckaert.be>
 ;;; Copyright © 2017, 2018, 2019, 2020 Paul Garlick <pgarlick@tourbillion-technology.com>
 ;;; Copyright © 2017, 2019 Arun Isaac <arunisaac@systemreboot.net>
 ;;; Copyright © 2017, 2018, 2019, 2020 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;; Copyright © 2017 Dave Love <me@fx@gnu.org>
-;;; Copyright © 2018, 2019 Jan Nieuwenhuizen <janneke@gnu.org>
+;;; Copyright © 2018, 2019, 2020 Jan Nieuwenhuizen <janneke@gnu.org>
 ;;; Copyright © 2018 Joshua Sierles, Nextjournal <joshua@nextjournal.com>
 ;;; Copyright © 2018 Nadya Voronova <voronovank@gmail.com>
 ;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
 ;;; Copyright © 2018, 2020 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
-;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018, 2021 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
-;;; Copyright © 2019 Nicolas Goaziou <mail@nicolasgoaziou.fr>
+;;; Copyright © 2019, 2021 Nicolas Goaziou <mail@nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
 ;;; Copyright © 2019 Robert Smith <robertsmith@posteo.net>
 ;;; Copyright © 2020 Jakub Kądziołka <kuba@kadziolka.net>
-;;; Copyright © 2020 Felix Gruber <felgru@posteo.net>
+;;; Copyright © 2020, 2021 Felix Gruber <felgru@posteo.net>
 ;;; Copyright © 2020 R Veera Kumar <vkor@vkten.in>
 ;;; Copyright © 2020 Vincent Legoll <vincent.legoll@gmail.com>
 ;;; Copyright © 2020 Nicolò Balzarotti <nicolo@nixo.xyz>
 ;;; Copyright © 2020 B. Wilson <elaexuotee@wilsonb.com>
-;;; Copyright © 2020 Vinicius Monego <monego@posteo.net>
+;;; Copyright © 2020, 2021 Vinicius Monego <monego@posteo.net>
+;;; Copyright © 2020 Simon Tournier <zimon.toutoune@gmail.com>
+;;; Copyright © 2020 Martin Becze <mjbecze@riseup.net>
+;;; Copyright © 2021 Gerd Heber <gerd.heber@gmail.com>
+;;; Copyright © 2021 Franck Pérignon <franck.perignon@univ-grenoble-alpes.fr>
+;;; Copyright © 2021 Philip McGrath <philip@philipmcgrath.com>
+;;; Copyright © 2021 Paul A. Patience <paul@apatience.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -69,6 +75,7 @@
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system glib-or-gtk)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
   #:use-module (guix build-system python)
   #:use-module (guix build-system ruby)
   #:use-module (gnu packages algebra)
   #:use-module (gnu packages check)
   #:use-module (gnu packages cmake)
   #:use-module (gnu packages compression)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages curl)
   #:use-module (gnu packages cyrus-sasl)
   #:use-module (gnu packages dbm)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages elf)
+  #:use-module (gnu packages emacs)
   #:use-module (gnu packages file)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages fltk)
   #:use-module (gnu packages less)
   #:use-module (gnu packages lisp)
   #:use-module (gnu packages linux)
+  #:use-module (gnu packages llvm)
   #:use-module (gnu packages logging)
   #:use-module (gnu packages lua)
   #:use-module (gnu packages gnome)
   #:use-module (gnu packages mpi)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages netpbm)
+  #:use-module (gnu packages ocaml)
   #:use-module (gnu packages onc-rpc)
   #:use-module (gnu packages pcre)
   #:use-module (gnu packages popt)
   #:use-module (gnu packages version-control)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
-  #:use-module (srfi srfi-1))
+  #:use-module (srfi srfi-1)
+  #:use-module (srfi srfi-26))
 
 (define-public aris
   (package
@@ -229,16 +241,19 @@ programming languages.")
 (define-public qhull
   (package
     (name "qhull")
-    (version "2019.1")
+    (version "2020.2")
     (source (origin
               (method url-fetch)
               (uri (string-append "http://www.qhull.org/download/qhull-"
                                   (car (string-split version #\.))
-                                  "-src-7.3.2.tgz"))
+                                  "-src-8.0.2.tgz"))
               (sha256
                (base32
-                "1ys3vh3qq0v9lh452xb932vp63advds1pxk42lk7cc1niiar0y9b"))))
+                "0zlbhg0lb6j60188c2xhcrvviskr079552icjldqhy1jhgmxghmm"))))
     (build-system cmake-build-system)
+    (arguments
+     `(#:configure-flags '("-DLINK_APPS_SHARED=ON"
+                           "-DCMAKE_POSITION_INDEPENDENT_CODE=ON")))
     (synopsis "Calculate convex hulls and related structures")
     (description
      "@code{Qhull} computes the convex hull, Delaunay triangulation, Voronoi
@@ -304,13 +319,13 @@ programming language.")
 (define-public units
   (package
    (name "units")
-   (version "2.19")
+   (version "2.21")
    (source (origin
             (method url-fetch)
             (uri (string-append "mirror://gnu/units/units-" version
                                 ".tar.gz"))
             (sha256 (base32
-                     "0mk562g7dnidjgfgvkxxpvlba66fh1ykmfd9ylzvcln1vxmi6qj2"))))
+                     "1bybhqs4yrly9myb5maz3kdmf8k4fhk2m1d5cbcryn40z6lq0gkc"))))
    (build-system gnu-build-system)
    (inputs
     `(("readline" ,readline)
@@ -515,7 +530,7 @@ numbers.")
 (define-public sleef
   (package
     (name "sleef")
-    (version "3.4.1")
+    (version "3.5.1")
     (source
      (origin
        (method git-fetch)
@@ -524,7 +539,7 @@ numbers.")
              (commit version)))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1gvf7cfvszmgjrsqivwmyy1jnp3hy80dmszxx827lhjz8yqq5019"))))
+        (base32 "1jybqrl2dvjxzg30xrhh847s375n2jr1pix644wi6hb5wh5mx3f7"))))
     (build-system cmake-build-system)
     (arguments
      '(#:configure-flags (list "-DCMAKE_BUILD_TYPE=Release"
@@ -559,7 +574,7 @@ It can utilize SIMD instructions that are available on modern processors.")
 (define-public glpk
   (package
     (name "glpk")
-    (version "4.65")
+    (version "5.0")
     (source
      (origin
       (method url-fetch)
@@ -567,12 +582,13 @@ It can utilize SIMD instructions that are available on modern processors.")
                           version ".tar.gz"))
       (sha256
        (base32
-        "040sfaa9jclg2nqdh83w71sv9rc1sznpnfiripjdyr48cady50a2"))))
+        "05bgxidxj8d9xdp82niy7cy36w181cxq7p8vc3y2ixshpgp1642a"))))
     (build-system gnu-build-system)
     (inputs
      `(("gmp" ,gmp)))
     (arguments
-     `(#:configure-flags '("--with-gmp")))
+     `(#:configure-flags '("--with-gmp"
+                           "--disable-static")))
     (home-page "https://www.gnu.org/software/glpk/")
     (synopsis "GNU Linear Programming Kit, supporting the MathProg language")
     (description
@@ -583,6 +599,20 @@ translator for the language.  In addition to the C library, a stand-alone
 LP/MIP solver is included in the package.")
     (license license:gpl3+)))
 
+(define-public glpk-4
+  (package
+    (inherit glpk)
+    (name "glpk")
+    (version "4.65")
+    (source
+     (origin
+      (method url-fetch)
+      (uri (string-append "mirror://gnu/glpk/glpk-"
+                          version ".tar.gz"))
+      (sha256
+       (base32
+        "040sfaa9jclg2nqdh83w71sv9rc1sznpnfiripjdyr48cady50a2"))))))
+
 (define-public 4ti2
   (package
     (name "4ti2")
@@ -640,7 +670,7 @@ computing convex hulls.")
 (define-public lrslib
   (package
     (name "lrslib")
-    (version "7.0a")
+    (version "7.1")
     (source
      (origin
        (method url-fetch)
@@ -649,7 +679,7 @@ computing convex hulls.")
                            (string-delete #\. version) ".tar.gz"))
        (sha256
         (base32
-         "034fa45r9hwx6ljmgpxk2872q34nklkalpdkc6s9hqw57rivi36k"))))
+         "05kq3hzam31dlmkccv3v358r478kpvx76mw37ka12c6ypwv5dsnk"))))
     (build-system gnu-build-system)
     (inputs
      `(("gmp" ,gmp)))
@@ -676,6 +706,30 @@ in memory, so even problems with very large output sizes can sometimes
 be solved.")
     (license license:gpl2+)))
 
+(define-public libcerf
+  (package
+    (name "libcerf")
+    (version "1.14")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://jugit.fz-juelich.de/mlz/libcerf")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "1ic2q7kvxpqmgxlishygvx8d00i4wn51vkq4fyac44ahhf6c3kwd"))))
+    (build-system cmake-build-system)
+    (native-inputs
+     `(("perl" ,perl)))
+    (home-page "https://jugit.fz-juelich.de/mlz/libcerf")
+    (synopsis "Library for complex error functions")
+    (description
+     "@code{libcerf} is a self-contained numeric library that provides an
+efficient and accurate implementation of complex error functions, along with
+Dawson, Faddeeva, and Voigt functions.")
+    (license license:expat)))
+
 (define-public vinci
   (package
     (name "vinci")
@@ -724,7 +778,7 @@ halfspaces) or by their double description with both representations.")
 (define-public arpack-ng
   (package
     (name "arpack-ng")
-    (version "3.6.3")
+    (version "3.8.0")
     (home-page "https://github.com/opencollab/arpack-ng")
     (source (origin
               (method git-fetch)
@@ -732,14 +786,16 @@ halfspaces) or by their double description with both representations.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1wljl96yqxc9v8r49c37lscwkdp58kaacfb9p6s6nvpm31haax4y"))))
+                "0l7as5z6xvbxly8alam9s4kws70952qq35a6vkljzayi4b9gbklx"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
        ("automake" ,automake)
-       ("libtool" ,libtool)))
+       ("libtool" ,libtool)
+       ("pkg-config" ,pkg-config)))
     (inputs
-     `(("lapack" ,lapack)
+     `(("eigen" ,eigen)
+       ("lapack" ,lapack)
        ("fortran" ,gfortran)))
     (synopsis "Fortran subroutines for solving eigenvalue problems")
     (description
@@ -752,16 +808,15 @@ large scale eigenvalue problems.")
   (package
     (inherit arpack-ng)
     (version "3.3.0")
-    (name (package-name arpack-ng))
-    (home-page (package-home-page arpack-ng))
     (source
      (origin
-       (method url-fetch)
-       (uri (string-append home-page "/archive/" version ".tar.gz"))
-       (file-name (string-append name "-" version ".tar.gz"))
+       (method git-fetch)
+       (uri (git-reference (url (package-home-page arpack-ng))
+                           (commit version)))
+       (file-name (git-file-name (package-name arpack-ng) version))
        (sha256
         (base32
-         "1cz53wqzcf6czmcpfb3vb61xi0rn5bwhinczl65hpmbrglg82ndd"))))))
+         "00h6bjvxjq7bv0b8pwnc0gw33ns6brlqv00xx2rh3w9b5n205918"))))))
 
 (define-public arpack-ng-openmpi
   (package (inherit arpack-ng)
@@ -809,6 +864,62 @@ problems in numerical linear algebra.")
     (license (license:non-copyleft "file://LICENSE"
                                 "See LICENSE in the distribution."))))
 
+(define-public clapack
+  (package
+    (name "clapack")
+    (version "3.2.1")
+    (source
+     (origin
+      (method url-fetch)
+      (uri (string-append "http://www.netlib.org/clapack/clapack-"
+                          version "-CMAKE.tgz"))
+      (sha256
+       (base32
+        "0nnap9q1mv14g57dl3vkvxrdr10k5w7zzyxs6rgxhia8q8mphgqb"))))
+    (build-system cmake-build-system)
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         ;; These tests use a lot of stack variables and segfault without
+         ;; lifting resource limits.
+         (add-after 'unpack 'disable-broken-tests
+           (lambda _
+             (substitute* "TESTING/CMakeLists.txt"
+               (("add_lapack_test.* xeigtstz\\)") ""))
+             #t))
+         (replace 'install
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let* ((out (assoc-ref outputs "out"))
+                    (libdir (string-append out "/lib"))
+                    (f2cinc (string-append out "/include/libf2c")))
+               (mkdir-p f2cinc)
+               (display (getcwd))
+               (for-each (lambda (file)
+                           (install-file file libdir))
+                         '("SRC/liblapack.a"
+                           "F2CLIBS/libf2c/libf2c.a"
+                           "TESTING/MATGEN/libtmglib.a"
+                           "BLAS/SRC/libblas.a"))
+               (for-each (lambda (file)
+                           (install-file file f2cinc))
+                         (cons "F2CLIBS/libf2c/arith.h"
+                               (find-files (string-append "../clapack-"
+                                                          ,version "-CMAKE/F2CLIBS/libf2c")
+                                           "\\.h$")))
+               (copy-recursively (string-append "../clapack-"
+                                                ,version "-CMAKE/INCLUDE")
+                                 (string-append out "/include"))
+               #t))))))
+    (home-page "https://www.netlib.org/clapack/")
+    (synopsis "Numerical linear algebra library for C")
+    (description
+     "The CLAPACK library was built using a Fortran to C conversion utility
+called f2c.  The entire Fortran 77 LAPACK library is run through f2c to obtain
+C code, and then modified to improve readability.  CLAPACK's goal is to
+provide LAPACK for someone who does not have access to a Fortran compiler.")
+    (license (license:non-copyleft "file://LICENSE"
+                                   "See LICENSE in the distribution."))))
+
 (define-public scalapack
   (package
     (name "scalapack")
@@ -845,14 +956,14 @@ singular value problems.")
 (define-public gnuplot
   (package
     (name "gnuplot")
-    (version "5.2.7")
+    (version "5.4.1")
     (source (origin
               (method url-fetch)
               (uri (string-append "mirror://sourceforge/gnuplot/gnuplot/"
                                   version "/gnuplot-"
                                   version ".tar.gz"))
        (sha256
-        (base32 "1vglp4la40f5dpj0zdj63zprrkyjgzy068p35bz5dqxjyczm1zlp"))))
+        (base32 "03jrqs5lvxmbbz2c4g17dn2hrxqwd3hfadk9q8wbkbkyas2h8sbb"))))
     (build-system gnu-build-system)
     (inputs `(("readline" ,readline)
               ("cairo" ,cairo)
@@ -864,7 +975,9 @@ singular value problems.")
        ("texlive" ,texlive-tiny)))
     (arguments `(#:configure-flags (list (string-append
                                           "--with-texdir=" %output
-                                          "/texmf-local/tex/latex/gnuplot"))))
+                                          "/texmf-local/tex/latex/gnuplot"))
+                 ;; Plot on a dumb terminal during tests.
+                 #:make-flags '("GNUTERM=dumb")))
     (home-page "http://www.gnuplot.info")
     (synopsis "Command-line driven graphing utility")
     (description "Gnuplot is a portable command-line driven graphing
@@ -997,10 +1110,10 @@ incompatible with HDF5.")
     (synopsis
      "HDF4 without netCDF API, can be combined with the regular netCDF library")))
 
-(define-public hdf5
+(define-public hdf5-1.8
   (package
     (name "hdf5")
-    (version "1.8.21")
+    (version "1.8.22")
     (source
      (origin
       (method url-fetch)
@@ -1015,9 +1128,8 @@ incompatible with HDF5.")
                                    (string-append major minor)))
                                 "/src/hdf5-" version ".tar.bz2")))
       (sha256
-       (base32 "03glk4w4wyb1jyb443g53y3y1ncnf6mj2cqwm6avfr2awkgb3cg5"))
-      (patches (search-patches "hdf5-config-date.patch"
-                               "hdf5-1.8-mpi-deprecations.patch"))))
+       (base32 "194ki2s5jrgl4czkvy5nc9nwjyapah0fj72l0gb0aysplp38i6v8"))
+      (patches (search-patches "hdf5-config-date.patch"))))
     (build-system gnu-build-system)
     (inputs
      `(("zlib" ,zlib)))
@@ -1066,7 +1178,7 @@ incompatible with HDF5.")
              ;; libhdf5.so.  We truncate the hashes to avoid
              ;; unnecessary store references to those compilers:
              (substitute* "src/libhdf5.settings"
-              (("(/gnu/store/)([a-Z0-9]*)" all prefix hash)
+              (("(/gnu/store/)([a-zA-Z0-9]*)" all prefix hash)
                (string-append prefix (string-take hash 10) "..."))
               ;; Don't record the build-time kernel version to make the
               ;; settings file reproducible.
@@ -1125,23 +1237,48 @@ extremely large and complex data collections.")
               "https://www.hdfgroup.org/ftp/HDF5/current/src/unpacked/COPYING"))))
 
 (define-public hdf5-1.10
-  (package (inherit hdf5)
-    (version "1.10.6")
+  (package
+    (inherit hdf5-1.8)
+    (version "1.10.7")
     (source
      (origin
-      (method url-fetch)
-      (uri (list (string-append "https://support.hdfgroup.org/ftp/HDF5/releases/"
-                                "hdf5-" (version-major+minor version)
-                                "/hdf5-" version "/src/hdf5-"
-                                version ".tar.bz2")
-                 (string-append "https://support.hdfgroup.org/ftp/HDF5/"
-                                "current"
-                                (apply string-append
-                                       (take (string-split version #\.) 2))
-                                "/src/hdf5-" version ".tar.bz2")))
-      (sha256
-       (base32 "1gf38x51128hn00744358w27xgzjk0ff4wra4yxh2lk804ck1mh9"))
-      (patches (search-patches "hdf5-config-date.patch"))))))
+       (method url-fetch)
+       (uri (list (string-append "https://support.hdfgroup.org/ftp/HDF5/releases/"
+                                 "hdf5-" (version-major+minor version)
+                                 "/hdf5-" version "/src/hdf5-"
+                                 version ".tar.bz2")
+                  (string-append "https://support.hdfgroup.org/ftp/HDF5/"
+                                 "current"
+                                 (apply string-append
+                                        (take (string-split version #\.) 2))
+                                 "/src/hdf5-" version ".tar.bz2")))
+       (sha256
+        (base32 "0pm5xxry55i0h7wmvc7svzdaa90rnk7h78rrjmnlkz2ygsn8y082"))
+       (patches (search-patches "hdf5-config-date.patch"))))))
+
+(define-public hdf5-1.12
+  (package
+    (inherit hdf5-1.8)
+    (version "1.12.0")
+    (source
+     (origin
+       (method url-fetch)
+       (uri (list (string-append "https://support.hdfgroup.org/ftp/HDF5/releases/"
+                                 "hdf5-" (version-major+minor version)
+                                 "/hdf5-" version "/src/hdf5-"
+                                 version ".tar.bz2")
+                  (string-append "https://support.hdfgroup.org/ftp/HDF5/"
+                                 "current"
+                                 (apply string-append
+                                        (take (string-split version #\.) 2))
+                                 "/src/hdf5-" version ".tar.bz2")))
+       (sha256
+        (base32 "0qazfslkqbmzg495jafpvqp0khws3jkxa0z7rph9qvhacil6544p"))
+       (patches (search-patches "hdf5-config-date.patch"))))))
+
+(define-public hdf5
+  ;; Default version of HDF5.
+  hdf5-1.10)
 
 (define-public hdf-java
   (package
@@ -1173,7 +1310,7 @@ extremely large and complex data collections.")
        ("slf4j-simple" ,java-slf4j-simple)))
     (inputs
      `(("hdf4" ,hdf4)
-       ("hdf5" ,hdf5)
+       ("hdf5" ,hdf5-1.8)
        ("zlib" ,zlib)
        ("libjpeg" ,libjpeg-turbo)
        ("slf4j-api" ,java-slf4j-api)))
@@ -1333,7 +1470,7 @@ System (Grid, Point and Swath).")
      `(("gfortran" ,gfortran)))
     (build-system gnu-build-system)
     (inputs
-     `(("hdf5" ,hdf5)
+     `(("hdf5" ,hdf5-1.8)
        ("zlib" ,zlib)
        ("gctp" ,gctp)))
     (arguments
@@ -1351,7 +1488,7 @@ Swath).")
     (license (license:non-copyleft home-page))))
 
 (define-public hdf5-parallel-openmpi
-  (package (inherit hdf5)
+  (package/inherit hdf5-1.10                      ;use the latest
     (name "hdf5-parallel-openmpi")
     (inputs
      `(("mpi" ,openmpi)
@@ -1377,7 +1514,7 @@ Swath).")
                (substitute* "testpar/Makefile"
                  (("(^TEST_PROG_PARA.*)t_pflush1(.*)" front back)
                   (string-append front back "\n")))
-               (substitute* "tools/h5diff/testph5diff.sh"
+               (substitute* "tools/test/h5diff/testph5diff.sh"
                  (("/bin/sh") (which "sh")))
                #t))))))
     (synopsis "Management suite for data with parallel IO support")))
@@ -1434,7 +1571,7 @@ Blosc-compressed datasets.")
         (base32
          "1gm76jbwhz9adbxgn14zx8cj33dmjdr2g5xcy0m9c2gakp8w59kj"))))
     (build-system gnu-build-system)
-    (inputs `(("hdf5" ,hdf5)))                 ;h5cc for tests
+    (inputs `(("hdf5" ,hdf5-1.8)))                ;h5cc for tests
     (home-page "https://www.hdfgroup.org/products/hdf5_tools/h5check.html")
     (synopsis "HDF5 format checker")
     (description "@code{h5check} is a validation tool for verifying that an
@@ -1476,17 +1613,17 @@ similar to MATLAB, GNU Octave or SciPy.")
 (define-public netcdf
   (package
     (name "netcdf")
-    (version "4.4.1.1")
+    (version "4.7.4")
     (source
      (origin
        (method url-fetch)
-       (uri (string-append "ftp://ftp.unidata.ucar.edu/pub/netcdf/"
-                           "netcdf-" version ".tar.gz"))
+       (uri (string-append
+             "https://www.unidata.ucar.edu/downloads/netcdf/ftp/"
+             "netcdf-c-" version ".tar.gz"))
        (sha256
         (base32
-         "1blc7ik5yin7i0ls2kag0a9xjk12m0dzx6v1x88az3ras3scci2d"))
-       (patches (search-patches "netcdf-date-time.patch"
-                                "netcdf-tst_h_par.patch"))))
+         "1a2fpp15a2rl1m50gcvvzd9y6bavl6vjf9zzf63sz5gdmq06yiqf"))
+       (patches (search-patches "netcdf-date-time.patch"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("m4" ,m4)
@@ -1495,6 +1632,7 @@ similar to MATLAB, GNU Octave or SciPy.")
     (inputs
      `(("hdf4" ,hdf4-alt)
        ("hdf5" ,hdf5)
+       ("curl" ,curl)
        ("zlib" ,zlib)
        ("libjpeg" ,libjpeg-turbo)))
     (arguments
@@ -1547,12 +1685,16 @@ sharing of scientific data.")
                 "--enable-parallel-tests"
                 ;; Shared libraries not supported with parallel IO.
                 "--disable-shared" "--with-pic"
-                ,flags))))))
+                ,flags))
+       ((#:phases phases '%standard-phases)
+        `(modify-phases ,phases
+           (add-after 'build 'mpi-setup
+             ,%openmpi-setup)))))))
 
 (define-public netcdf-fortran
   (package
     (name "netcdf-fortran")
-    (version "4.4.4")
+    (version "4.5.3")
     (source (origin
               (method url-fetch)
               (uri (string-append
@@ -1560,7 +1702,7 @@ sharing of scientific data.")
                     version ".tar.gz"))
               (sha256
                (base32
-                "0xaxdcg1p83zmypwml3swsnr3ccn38inwldyr1l3wa4dbwbrblxj"))))
+                "0x4acvfhbsx1q79dkkwrwbgfhm0w5ngnp4zj5kk92s1khihmqfhj"))))
     (build-system gnu-build-system)
     (arguments
      `(#:parallel-tests? #f))
@@ -1614,21 +1756,16 @@ online as well as original implementations of various other algorithms.")
 (define-public ipopt
   (package
     (name "ipopt")
-    (version "3.12.12")
+    (version "3.13.4")
     (source (origin
-              (method url-fetch)
-              (uri (string-append
-                    "https://www.coin-or.org/download/source/Ipopt/Ipopt-"
-                    version".tgz"))
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/coin-or/Ipopt")
+                    (commit (string-append "releases/" version))))
+              (file-name (git-file-name name version))
               (sha256
                (base32
-                "07yn9rzdswjk8n246qq6ci9ssf2bcplkifcpsfz9j6cdxw9vgbkv"))
-              (modules '((guix build utils)))
-              (snippet
-               ;; Make sure we don't use the bundled software.
-               '(begin
-                  (delete-file-recursively "ThirdParty")
-                  #t))))
+                "08gznhwhqv1x4baksz350ih8q16r5rd0k8vals6078m3h94khr4b"))))
     (build-system gnu-build-system)
     (arguments
      '(#:phases (modify-phases %standard-phases
@@ -1648,7 +1785,8 @@ online as well as original implementations of various other algorithms.")
                                           after "\n")))
                         #t))))))
     (native-inputs
-     `(("gfortran" ,gfortran)))
+     `(("gfortran" ,gfortran)
+       ("pkg-config" ,pkg-config)))
     (inputs
      ;; TODO: Maybe add dependency on COIN-MUMPS, ASL, and HSL.
      `(("lapack" ,lapack)))                    ;for both libblas and liblapack
@@ -1658,6 +1796,35 @@ online as well as original implementations of various other algorithms.")
      "The Interior Point Optimizer (IPOPT) is a software package for
 large-scale nonlinear optimization.  It provides C++, C, and Fortran
 interfaces.")
+    (license license:epl2.0)))
+
+(define-public cbc
+  (package
+    (name "cbc")
+    (version "2.10.5")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://www.coin-or.org/download/source/"
+                                  "Cbc/Cbc-" version ".tgz"))
+              (sha256
+               (base32
+                "0wk9vr6zc62gw71v7gnra5wxqlcljcgbhm5lasx236v791b986ns"))
+              (modules '((guix build utils)))
+              (snippet
+               ;; Make sure we don't use the bundled software.
+               '(delete-file-recursively "ThirdParty"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("gfortran" ,gfortran)
+       ("pkg-config" ,pkg-config)))
+    (inputs
+     `(("openblas" ,openblas)))
+    (home-page "https://www.coin-or.org")
+    (synopsis "Branch-and-cut solver")
+    (description
+     "Cbc (Coin-or branch and cut) is a mixed integer linear programming
+solver written in C++.  It can be used as a library or as a standalone
+executable.")
     (license license:epl1.0)))
 
 (define-public clp
@@ -1692,6 +1859,84 @@ linear and quadratic objectives.  There are limited facilities for nonlinear
 and quadratic objectives using the Simplex algorithm.")
     (license license:epl1.0)))
 
+(define-public libflame
+  (package
+    (name "libflame")
+    (version "5.2.0")
+    (outputs '("out" "static"))
+    (source
+      (origin
+        (method git-fetch)
+        (uri (git-reference
+               (url "https://github.com/flame/libflame")
+               (commit version)))
+        (file-name (git-file-name name version))
+        (sha256
+         (base32
+          "1n6lf0wvpp77lxqlr721h2jbfbzigphdp19wq8ajiccilcksh7ay"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:configure-flags
+       ;; Sensible defaults: https://github.com/flame/libflame/issues/28
+       (list "--enable-dynamic-build"
+             "--enable-max-arg-list-hack"
+             "--enable-lapack2flame"
+             "--enable-verbose-make-output"
+             "--enable-multithreading=pthreads" ; Openblas isn't built with openmp.
+             ,@(if (any (cute string-prefix? <> (or (%current-target-system)
+                                                    (%current-system)))
+                        '("x86_64" "i686"))
+                 '("--enable-vector-intrinsics=sse")
+                 '())
+             "--enable-supermatrix"
+             "--enable-memory-alignment=16"
+             "--enable-ldim-alignment")
+       #:phases
+       (modify-phases %standard-phases
+         (add-after 'unpack 'patch-/usr/bin/env-bash
+           (lambda _
+             (substitute* "build/config.mk.in"
+               (("/usr/bin/env bash") (which "bash")))
+             #t))
+         (replace 'check
+           (lambda* (#:key tests? #:allow-other-keys)
+             (substitute* "test/Makefile"
+               (("LIBBLAS .*") "LIBBLAS = -lblas\n")
+               (("LIBLAPACK .*") "LIBLAPACK = -llapack\n"))
+             (if tests?
+               (with-directory-excursion "test"
+                 (mkdir "obj")
+                 (invoke "make")
+                 (invoke "./test_libflame.x"))
+               #t)))
+         (add-after 'install 'install-static
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out"))
+                   (static (assoc-ref outputs "static")))
+               (mkdir-p (string-append static "/lib"))
+               (rename-file (string-append out "/lib/libflame.a")
+                            (string-append static "/lib/libflame.a"))
+               (install-file (string-append out "/include/FLAME.h")
+                             (string-append static "/include"))
+               #t))))))
+    (inputs
+     `(("gfortran" ,gfortran)))
+    (native-inputs
+     `(("lapack" ,lapack)
+       ("openblas" ,openblas)
+       ("perl" ,perl)
+       ("python" ,python-wrapper)))
+    (home-page "https://github.com/flame/libflame")
+    (synopsis "High-performance object-based library for DLA computations")
+    (description "@code{libflame} is a portable library for dense matrix
+computations, providing much of the functionality present in LAPACK, developed
+by current and former members of the @acronym{SHPC, Science of High-Performance
+Computing} group in the @url{https://www.ices.utexas.edu/, Institute for
+Computational Engineering and Sciences} at The University of Texas at Austin.
+@code{libflame} includes a compatibility layer, @code{lapack2flame}, which
+includes a complete LAPACK implementation.")
+    (license license:bsd-3)))
+
 (define-public ceres
   (package
     (name "ceres-solver")
@@ -1745,15 +1990,15 @@ can solve two kinds of problems:
 (define-public octave-cli
   (package
     (name "octave-cli")
-    (version "5.2.0")
+    (version "6.2.0")
     (source
      (origin
       (method url-fetch)
       (uri (string-append "mirror://gnu/octave/octave-"
-                          version ".tar.lz"))
+                          version ".tar.xz"))
       (sha256
        (base32
-        "1848dq6nxzal8gwjrcp6xhi5gq96w89nss9d9rz75q408gb3mbl6"))))
+        "06id09zspya24gshcwgp039cp35c06150mdlxysawgnbrhj16wkv"))))
     (build-system gnu-build-system)
     (inputs
      `(("alsa-lib" ,alsa-lib)
@@ -1788,8 +2033,7 @@ can solve two kinds of problems:
        ("texinfo" ,texinfo)
        ("zlib" ,zlib)))
     (native-inputs
-     `(("lzip" ,lzip)
-       ("gfortran" ,gfortran)
+     `(("gfortran" ,gfortran)
        ("pkg-config" ,pkg-config)
        ("perl" ,perl)
        ;; The following inputs are not actually used in the build process.
@@ -1829,7 +2073,7 @@ can solve two kinds of problems:
                  "\"" (assoc-ref inputs "texinfo") "/bin/makeinfo\"")))
              #t)))))
     (home-page "https://www.gnu.org/software/octave/")
-    (synopsis "High-level language for numerical computation")
+    (synopsis "High-level language for numerical computation (no GUI)")
     (description "GNU Octave is a high-level interpreted language that is
 specialized for numerical computations.  It can be used for both linear and
 non-linear applications and it provides great support for visualizing results.
@@ -1840,8 +2084,6 @@ script files.")
 (define-public octave
   (package (inherit octave-cli)
     (name "octave")
-    (source (origin
-              (inherit (package-source octave-cli))))
     (inputs
      `(("qscintilla" ,qscintilla)
        ("qt" ,qtbase)
@@ -1863,7 +2105,8 @@ script files.")
                (substitute* "configure"
                  (("qscintilla2-qt5")
                   "qscintilla2_qt5"))
-               #t))))))))
+               #t))))))
+    (synopsis "High-level language for numerical computation (with GUI)")))
 
 (define-public opencascade-oce
   (package
@@ -2015,7 +2258,7 @@ This is the certified version of the Open Cascade Technology (OCCT) library.")
 (define-public gmsh
   (package
     (name "gmsh")
-    (version "2.16.0")
+    (version "4.6.0")
     (source
      (origin
       (method git-fetch)
@@ -2027,12 +2270,11 @@ This is the certified version of the Open Cascade Technology (OCCT) library.")
                                         version)))))
       (file-name (git-file-name name version))
       (sha256
-       (base32 "08rq4jajwmlpivnm9yifz2jhaivnz065lnk0h2zv773nwl9wf162"))
+       (base32 "0m0pjxcy1bnr7a20i11lh0ih159pphq9wsvfjr3sfx4y3lginz5y"))
       (modules '((guix build utils)))
       (snippet
-       ;; Remove non-free METIS code
        '(begin
-          (delete-file-recursively "contrib/Metis")
+          (delete-file-recursively "contrib/metis")
           #t))))
     (build-system cmake-build-system)
     (propagated-inputs
@@ -2043,14 +2285,15 @@ This is the certified version of the Open Cascade Technology (OCCT) library.")
        ("lapack" ,lapack)
        ("mesa" ,mesa)
        ("glu" ,glu)
-       ("opencascade-oce" ,opencascade-oce)
+       ("metis" ,metis)
+       ("opencascade-occt" ,opencascade-occt)
        ("libx11" ,libx11)
        ("libxext" ,libxext)))
     (inputs
      `(("fontconfig" ,fontconfig)
        ("libxft" ,libxft)))
     (arguments
-     `(#:configure-flags `("-DENABLE_METIS:BOOL=OFF"
+     `(#:configure-flags `("-DENABLE_SYSTEM_CONTRIB:BOOL=ON"
                            "-DENABLE_BUILD_SHARED:BOOL=ON"
                            "-DENABLE_BUILD_DYNAMIC:BOOL=ON")))
     (home-page "http://gmsh.info/")
@@ -2064,6 +2307,71 @@ modules is done either interactively using the graphical user interface or in
 ASCII text files using Gmsh's own scripting language.")
     (license license:gpl2+)))
 
+(define-public veusz
+  (package
+    (name "veusz")
+    (version "3.3.1")
+    (source
+     (origin
+       (method url-fetch)
+       (uri (pypi-uri "veusz" version))
+       (sha256
+        (base32 "1q7hi1qwwg4pgiz62isvv1pia85m13bspdpp1q3mrnwl11in0ag0"))))
+    (build-system python-build-system)
+    (arguments
+     `(;; Tests will fail because they depend on optional packages like
+       ;; python-astropy, which is not packaged.
+       #:tests? #f
+       #:phases
+       (modify-phases %standard-phases
+         ;; Veusz will append 'PyQt5' to sip_dir by default. That is not how
+         ;; the path is defined in Guix, therefore we have to change it.
+         (add-after 'unpack 'fix-sip-dir
+           (lambda _
+             (substitute* "pyqtdistutils.py"
+               (("os.path.join\\(sip_dir, 'PyQt5'\\)") "sip_dir"))
+             #t))
+         ;; Now we have to pass the correct sip_dir to setup.py.
+         (replace 'build
+           (lambda* (#:key inputs #:allow-other-keys)
+             ;; We need to tell setup.py where to locate QtCoremod.sip
+             ((@@ (guix build python-build-system) call-setuppy)
+              "build_ext"
+              (list (string-append "--sip-dir="
+                                   (assoc-ref inputs "python-pyqt")
+                                   "/share/sip"))
+              #t)))
+         ;; Ensure that icons are found at runtime.
+         (add-after 'install 'wrap-executable
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               (wrap-program (string-append out "/bin/veusz")
+                 `("QT_PLUGIN_PATH" prefix
+                   ,(list (string-append (assoc-ref inputs "qtsvg")
+                                         "/lib/qt5/plugins/"))))))))))
+    (native-inputs
+     `(("pkg-config" ,pkg-config)
+       ;;("python-astropy" ,python-astropy) ;; FIXME: Package this.
+       ("qttools" ,qttools)
+       ("python-sip" ,python-sip-4)))
+    (inputs
+     `(("ghostscript" ,ghostscript) ;optional, for EPS/PS output
+       ("python-dbus" ,python-dbus)
+       ("python-h5py" ,python-h5py) ;optional, for HDF5 data
+       ("python-pyqt" ,python-pyqt)
+       ("qtbase" ,qtbase)
+       ("qtsvg" ,qtsvg)))
+    (propagated-inputs
+     `(("python-numpy" ,python-numpy)))
+    (home-page "https://veusz.github.io/")
+    (synopsis "Scientific plotting package")
+    (description
+     "Veusz is a scientific plotting and graphing program with a graphical
+user interface, designed to produce publication-ready 2D and 3D plots.  In
+addition it can be used as a module in Python for plotting.  It supports
+vector and bitmap output, including PDF, Postscript, SVG and EMF.")
+    (license license:gpl2+)))
+
 (define-public maxflow
   (package
     (name "maxflow")
@@ -2263,7 +2571,18 @@ scientific applications modeled by partial differential equations.")
         (uri (pypi-uri "petsc4py" version))
         (sha256
           (base32
-            "1rm1qj5wlkhxl39by9n78lh3gbmii31wsnb8j1rr5hvfr5xgbx2q"))))
+           "1rm1qj5wlkhxl39by9n78lh3gbmii31wsnb8j1rr5hvfr5xgbx2q"))
+        (modules '((guix build utils)))
+        (snippet
+         '(begin
+            ;; Ensure source file is regenerated in the build phase.
+            (delete-file "src/petsc4py.PETSc.c")
+            ;; Remove legacy GC code.  See
+            ;; https://bitbucket.org/petsc/petsc4py/issues/125.
+            (substitute* "src/PETSc/cyclicgc.pxi"
+                         ((".*gc_refs.*") "" )
+                         ((".*PyGC_Head.*") ""))
+            #t))))
     (build-system python-build-system)
     (arguments
      `(#:phases
@@ -2275,6 +2594,8 @@ scientific applications modeled by partial differential equations.")
              #t))
          (add-before 'check 'mpi-setup
            ,%openmpi-setup))))
+    (native-inputs
+     `(("python-cython" ,python-cython)))
     (inputs
      `(("petsc" ,petsc-openmpi)
        ("python-numpy" ,python-numpy)))
@@ -2378,7 +2699,7 @@ savings are consistently > 5x.")
                           "test.log" "error.log" "RDict.db"
                           "uninstall.py"))
               #t))))))
-    (home-page "http://slepc.upv.es")
+    (home-page "https://slepc.upv.es")
     (synopsis "Scalable library for eigenproblems")
     (description "SLEPc is a software library for the solution of large sparse
 eigenproblems on parallel computers.  It can be used for the solution of
@@ -2463,7 +2784,7 @@ bindings to almost all functions of SLEPc.")
 (define-public metamath
   (package
     (name "metamath")
-    (version "0.183")
+    (version "0.193")
     (source
      (origin
        (method git-fetch)
@@ -2472,7 +2793,7 @@ bindings to almost all functions of SLEPc.")
              (commit (string-append "v" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1jjf4fy6j53i40dh0yv0f9sngnw4gs24cig99vsg3q0303pwrhg7"))))
+        (base32 "1s9hyknfvhj86g3giayyf3dxzg23iij0rs7bdvj075v9qbyhqn9b"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -2688,14 +3009,14 @@ easy-to-write markup language for mathematics.")
 (define-public superlu
   (package
     (name "superlu")
-    (version "5.2.1")
+    (version "5.2.2")
     (source
      (origin
        (method url-fetch)
        (uri (string-append "https://portal.nersc.gov/project/sparse/superlu/"
                            "superlu_" version ".tar.gz"))
        (sha256
-        (base32 "0qzlb7cd608q62kyppd0a8c65l03vrwqql6gsm465rky23b6dyr8"))
+        (base32 "13520vk6fqspyl22cq4ak2jh3rlmhja4czq56j75fdx65fkk80s7"))
        (modules '((guix build utils)))
        (snippet
         ;; Replace the non-free implementation of MC64 with a stub adapted
@@ -2754,18 +3075,21 @@ also provides threshold-based ILU factorization preconditioners.")
 (define-public superlu-dist
   (package
     (name "superlu-dist")
-    (version "6.2.0")
+    (version "6.4.0")
     (source
      (origin
-       (method url-fetch)
-       (uri (string-append "https://portal.nersc.gov/project/sparse/superlu/"
-                           "superlu_dist_" version ".tar.gz"))
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/xiaoyeli/superlu_dist")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
        (sha256
-        (base32 "1ynmwqajc9sc3my2hssa5k9s58ggvizqv9rdss0j7w99pbh5mnvw"))
+        (base32 "0fa29yr72p4yq5ln4rgfsawmi5935n4qcr5niz6864bjladz4lql"))
        (modules '((guix build utils)))
        (snippet
         ;; Replace the non-free implementation of MC64 with a stub
         '(begin
+           (make-file-writable "SRC/mc64ad_dist.c")
            (call-with-output-file "SRC/mc64ad_dist.c"
              (lambda (port)
                (display "
@@ -2843,14 +3167,14 @@ implemented in ANSI C, and MPI for communications.")
 (define-public scotch
   (package
     (name "scotch")
-    (version "6.0.6")
+    (version "6.1.0")
     (source
      (origin
       (method url-fetch)
       (uri (string-append "https://gforge.inria.fr/frs/download.php/"
                           "latestfile/298/scotch_" version ".tar.gz"))
       (sha256
-       (base32 "1ky4k9r6jvajhqaqnnx6h8fkmds2yxgp70dpr1qzwcyhi2nhqvv8"))
+       (base32 "1184fcv4wa2df8szb5lan6pjh0raarr45pk8ilpvbz23naikzg53"))
       (patches (search-patches "scotch-build-parallelism.patch"
                                "scotch-integer-declarations.patch"))))
     (build-system gnu-build-system)
@@ -2898,7 +3222,7 @@ YACC = bison -pscotchyy -y -b y
                           "COMMON_PTHREAD"
                           "COMMON_RANDOM_FIXED_SEED"
                           "INTSIZE64"             ;use 'int64_t'
-                          ;; Prevents symbolc clashes with libesmumps
+                          ;; Prevents symbol clashes with libesmumps
                           "SCOTCH_RENAME"
                           ;; XXX: Causes invalid frees in superlu-dist tests
                           ;; "SCOTCH_PTHREAD"
@@ -2986,6 +3310,63 @@ YACC = bison -pscotchyy -y -b y
     (synopsis
      "Programs and libraries for graph algorithms (32-bit integers)")))
 
+(define-public scotch-shared
+  (package (inherit scotch)
+    (name "scotch-shared")
+    (native-inputs
+     `(("gcc" ,gcc)
+       ("flex" ,flex)
+       ("bison" ,bison)))
+    (arguments
+     (substitute-keyword-arguments (package-arguments scotch)
+       ((#:phases scotch-shared-phases)
+        `(modify-phases ,scotch-shared-phases
+           (replace
+            'configure
+           (lambda _
+             ;; Otherwise, the RUNPATH will lack the final path component.
+             (setenv "RPATHFLAGS" (string-append "-Wl,-rpath="
+                                              (assoc-ref %outputs "out") "/lib"))
+            (call-with-output-file "Makefile.inc"
+              (lambda (port)
+                (format port "
+EXE =
+LIB = .so
+OBJ = .o
+MAKE = make
+AR = gcc
+ARFLAGS = -shared -o
+CAT = cat
+CCS = gcc
+CCP = mpicc
+CCD = gcc
+CPPFLAGS =~{ -D~a~}
+CFLAGS = -O2 -g -fPIC $(CPPFLAGS) $(RPATHFLAGS)
+CLIBFLAGS = -shared -fPIC
+LDFLAGS = -lz -lm -lrt -lpthread -Xlinker --no-as-needed
+CP = cp
+LEX = flex -Pscotchyy -olex.yy.c
+LN = ln
+MKDIR = mkdir
+MV = mv
+RANLIB = echo
+YACC = bison -pscotchyy -y -b y
+"
+                        '("COMMON_FILE_COMPRESS_GZ"
+                          "COMMON_PTHREAD"
+                          "COMMON_RANDOM_FIXED_SEED"
+                          "INTSIZE64"             ;use 'int64_t'
+                          ;; Prevents symbolc clashes with libesmumps
+                          "SCOTCH_RENAME"
+                          ;; XXX: Causes invalid frees in superlu-dist tests
+                          ;; "SCOTCH_PTHREAD"
+                          ;; "SCOTCH_PTHREAD_NUMBER=2"
+                          "restrict=__restrict"
+                          ))))#t))
+           (delete 'check)))))
+     (synopsis
+      "Programs and libraries for graph algorithms (shared libraries version)")))
+
 (define-public pt-scotch
   (package (inherit scotch)
     (name "pt-scotch")
@@ -3033,6 +3414,28 @@ YACC = bison -pscotchyy -y -b y
     (synopsis
      "Programs and libraries for graph algorithms (with MPI and 32-bit integers)")))
 
+(define-public pt-scotch-shared
+  (package (inherit scotch-shared)
+    (name "pt-scotch-shared")
+    (propagated-inputs
+     `(("openmpi" ,openmpi)))           ;Headers include MPI headers
+    (arguments
+     (substitute-keyword-arguments (package-arguments scotch-shared)
+       ((#:phases scotch-shared-phases)
+        `(modify-phases ,scotch-shared-phases
+           (replace
+            'build
+            (lambda _
+              (invoke "make" (format #f "-j~a" (parallel-job-count))
+                      "ptscotch" "ptesmumps")
+
+              ;; Install the serial metis compatibility library
+              (invoke "make" "-C" "libscotchmetis" "install")))
+           (add-before 'check 'mpi-setup
+             ,%openmpi-setup)))))
+    (synopsis "Graph algorithms (shared libraries version, with MPI)")))
+
+
 (define-public metis
   (package
     (name "metis")
@@ -3045,6 +3448,9 @@ YACC = bison -pscotchyy -y -b y
        (sha256
         (base32
          "1cjxgh41r8k6j029yxs8msp3z6lcnpm16g5pvckk35kc7zhfpykn"))))
+    (properties
+     `((release-monitoring-url
+        . "http://glaros.dtc.umn.edu/gkhome/metis/metis/download")))
     (build-system cmake-build-system)
     (inputs
      `(("blas" ,openblas)))
@@ -3263,7 +3669,7 @@ point numbers.")
 (define-public wxmaxima
   (package
     (name "wxmaxima")
-    (version "20.04.0")
+    (version "21.04.0")
     (source
      (origin
        (method git-fetch)
@@ -3272,13 +3678,10 @@ point numbers.")
              (commit (string-append "Version-" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "0vrjxzfgmjdzm1rgl0crz4b4badl14jwh032y3xkcdvjl5j67lp3"))))
+        (base32 "0xj95zk16x8kac8qhzd5kvf3b00x7hgdw85da9ww63xyndvhh2lw"))))
     (build-system cmake-build-system)
     (native-inputs
-     `(("gettext" ,gettext-minimal)
-       ("xorg-server" ,xorg-server-for-tests)))
-    ;; TODO: Add libomp for multithreading support.
-    ;; As of right now, enabling libomp causes the imageCells.wxm test to fail.
+     `(("gettext" ,gettext-minimal)))
     (inputs
      `(("wxwidgets" ,wxwidgets)
        ("maxima" ,maxima)
@@ -3287,15 +3690,16 @@ point numbers.")
        ("gtk+" ,gtk+)
        ("shared-mime-info" ,shared-mime-info)))
     (arguments
-     `(#:test-target "test"
+     `(#:tests? #f                      ; tests fail non-deterministically
        #:phases
        (modify-phases %standard-phases
-         (add-before 'check 'pre-check
+         (add-after 'unpack 'patch-doc-path
            (lambda _
-             ;; Tests require a running X server.
-             (system "Xvfb :1 &")
-             (setenv "DISPLAY" ":1")
-             (setenv "HOME" (getcwd))
+             ;; Don't look in share/doc/wxmaxima-xx.xx.x for the
+             ;; documentation.  Only licensing information is placed there by
+             ;; Guix.
+             (substitute* "src/Dirstructure.cpp"
+               (("/doc/wxmaxima-\\%s") "/doc/wxmaxima"))
              #t))
          (add-after 'install 'wrap-program
            (lambda* (#:key inputs outputs #:allow-other-keys)
@@ -3483,52 +3887,94 @@ parts of it.")
     (synopsis "Optimized BLAS library based on GotoBLAS (ILP64 version)")
     (license license:bsd-3)))
 
-(define* (make-blis implementation #:optional substitutable?)
-  "Return a BLIS package with the given IMPLEMENTATION (see config/ in the
-source tree for a list of implementations.)
-
-SUBSTITUTABLE? determines whether the package is made available as a
-substitute.
-
-Currently the specialization must be selected at configure-time, but work is
-underway to allow BLIS to select the right optimized kernels at run time:
-<https://github.com/flame/blis/issues/129>."
+(define-public blis
   (package
-    (name (if (string=? implementation "reference")
-              "blis"
-              (string-append "blis-" implementation)))
-    (version "0.2.2")
+    (name "blis")
+    (version "0.8.1")
     (home-page "https://github.com/flame/blis")
     (source (origin
               (method git-fetch)
               (uri (git-reference (url home-page) (commit version)))
               (sha256
                (base32
-                "1wr79a50nm4abhw8w3sn96nmwp5mrzifcigk7khw9qcgyyyqayfh"))
+                "05ifil6jj9424sr8kmircl8k4bmxnl3y12a79vwj1kxxva5gz50g"))
               (file-name (git-file-name "blis" version))))
+    (native-inputs
+     `(("python" ,python)
+       ("perl" ,perl)))
     (build-system gnu-build-system)
     (arguments
-     `(#:test-target "test"
-
-       #:substitutable? ,substitutable?
-
-       #:phases (modify-phases %standard-phases
-                  (replace 'configure
-                    (lambda* (#:key outputs #:allow-other-keys)
-                      ;; This is a home-made 'configure' script.
-                      (let ((out (assoc-ref outputs "out")))
-                        (invoke "./configure" "-p" out
-                                "-d" "opt"
-                                "--disable-static"
-                                "--enable-shared"
-                                "--enable-threading=openmp"
-
-                                ,implementation))))
-                  (add-before 'check 'show-test-output
-                    (lambda _
-                      ;; By default "make check" is silent.  Make it verbose.
-                      (system "tail -F output.testsuite &")
-                      #t)))))
+     `(#:modules
+       ((guix build gnu-build-system)
+        (guix build utils)
+        (srfi srfi-1))
+        #:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key outputs
+                           target
+                           system
+                           (configure-flags '())
+                           #:allow-other-keys)
+             ;; This is a home-made 'configure' script.
+             (let* ((out (assoc-ref outputs "out"))
+                     ;; Guix-specific support for choosing the configuration
+                     ;; via #:configure-flags: see below for details.
+                    (config-flag-prefix "--blis-config=")
+                    (maybe-config-flag (find
+                                        (lambda (s)
+                                          (string-prefix? config-flag-prefix s))
+                                        configure-flags))
+                    (configure-flags (if maybe-config-flag
+                                         (delete maybe-config-flag
+                                                 configure-flags)
+                                         configure-flags))
+                    ;; Select the "configuration" to build.
+                    ;; The "generic" configuration is non-optimized but
+                    ;; portable (no assembly).
+                    ;; The "x86_64" configuration family includes
+                    ;; sub-configurations for all supported
+                    ;; x86_64 microarchitectures.
+                    ;; BLIS currently lacks runtime hardware detection
+                    ;; for other architectures: see
+                    ;; <https://github.com/flame/blis/commit/c534da6>.
+                    ;; Conservatively, we stick to "generic" on armhf,
+                    ;; aarch64, and ppc64le for now. (But perhaps
+                    ;; "power9", "cortexa9", and "cortexa57" might be
+                    ;; general enough to use?)
+                    ;; Another approach would be to use the "auto"
+                    ;; configuration and make this package
+                    ;; non-substitutable.
+                    ;; The build is fairly intensive, though.
+                    (blis-config
+                     (cond
+                      (maybe-config-flag
+                       (substring maybe-config-flag
+                                  (string-length config-flag-prefix)))
+                      ((string-prefix? "x86_64" (or target system))
+                       "x86_64")
+                      (else
+                       "generic")))
+                    (configure-args
+                     `("-p" ,out
+                       "-d" "opt"
+                       "--disable-static"
+                       "--enable-shared"
+                       "--enable-threading=openmp"
+                       "--enable-verbose-make"
+                       ,@configure-flags
+                       ,blis-config)))
+               (format #t "configure args: ~s~%" configure-args)
+               (apply invoke
+                      "./configure"
+                      configure-args)
+               #t)))
+         (add-before 'check 'show-test-output
+           (lambda _
+             ;; By default "make check" is silent.  Make it verbose.
+             (system "tail -F output.testsuite &")
+             #t)))))
     (synopsis "High-performance basic linear algebra (BLAS) routines")
     (description
      "BLIS is a portable software framework for instantiating high-performance
@@ -3540,35 +3986,12 @@ it also includes a BLAS compatibility layer which gives application developers
 access to BLIS implementations via traditional BLAS routine calls.")
     (license license:bsd-3)))
 
-(define-public blis
-  ;; This is the "reference" implementation, which is the non-optimized but
-  ;; portable variant (no assembly).
-  (make-blis "reference" #t))
+(define-public blis-sandybridge (deprecated-package "blis-sandybridge" blis))
+(define-public blis-haswell (deprecated-package "blis-haswell" blis))
+(define-public blis-knl (deprecated-package "blis-knl" blis))
 
 (define ignorance blis)
 
-(define-syntax-rule (blis/x86_64 processor)
-  "Expand to a package specialized for PROCESSOR."
-  (package
-    (inherit (make-blis processor))
-    (supported-systems '("x86_64-linux"))))
-
-(define-public blis-sandybridge
-  ;; BLIS specialized for Sandy Bridge processors (launched 2011):
-  ;; <http://ark.intel.com/products/codename/29900/Sandy-Bridge>.
-  (blis/x86_64 "sandybridge"))
-
-(define-public blis-haswell
-  ;; BLIS specialized for Haswell processors (launched 2013):
-  ;; <http://ark.intel.com/products/codename/42174/Haswell>.
-  (blis/x86_64 "haswell"))
-
-(define-public blis-knl
-  ;; BLIS specialized for Knights Landing processor (launched 2016):
-  ;; <http://ark.intel.com/products/series/92650/Intel-Xeon-Phi-x200-Product-Family>.
-  (blis/x86_64 "knl"))
-
-
 (define-public openlibm
   (package
     (name "openlibm")
@@ -3649,7 +4072,7 @@ Fresnel integrals, and similar related functions as well.")
 (define-public suitesparse
   (package
     (name "suitesparse")
-    (version "5.7.1")
+    (version "5.9.0")
     (source
      (origin
        (method git-fetch)
@@ -3659,7 +4082,7 @@ Fresnel integrals, and similar related functions as well.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "174p3l78kv9gaa0i5hflyai2ydwnjzh34k9938sl4aa3li0543s8"))
+         "1zhkix58afw92s7p291prljdm3yi0pjg1kbi3lczdb8rb14jkz5n"))
        (patches (search-patches "suitesparse-mongoose-cmake.patch"))
        (modules '((guix build utils)))
        (snippet
@@ -3669,10 +4092,9 @@ Fresnel integrals, and similar related functions as well.")
            #t))))
     (build-system gnu-build-system)
     (arguments
-     '(#:tests? #f  ;no "check" target
+     `(#:tests? #f  ;no "check" target
        #:make-flags
-       (list "CC=gcc"
-             "BLAS=-lblas"
+       (list (string-append "CC=" ,(cc-for-target))
              "TBB=-ltbb"
              "MY_METIS_LIB=-lmetis"
              ;; Flags for cmake (required to build GraphBLAS and Mongoose)
@@ -3682,7 +4104,8 @@ Fresnel integrals, and similar related functions as well.")
                             " -DCMAKE_C_FLAGS_RELEASE=\"$(CFLAGS) $(CPPFLAGS)\""
                             " -DCMAKE_CXX_FLAGS_RELEASE=\"$(CXXFLAGS) $(CPPFLAGS)\""
                             " -DCMAKE_SKIP_RPATH=TRUE"
-                            " -DCMAKE_BUILD_TYPE=Release")
+                            " -DCMAKE_BUILD_TYPE=Release"
+                            " -DCMAKE_INSTALL_LIBDIR=lib")
              (string-append "INSTALL_LIB="
                             (assoc-ref %outputs "out") "/lib")
              (string-append "INSTALL_INCLUDE="
@@ -3694,6 +4117,8 @@ Fresnel integrals, and similar related functions as well.")
     (inputs
      `(("tbb" ,tbb)
        ("lapack" ,lapack)
+       ("gmp" ,gmp)
+       ("mpfr" ,mpfr)
        ("metis" ,metis)))
     (native-inputs
      `(("cmake" ,cmake-minimal)
@@ -3838,6 +4263,34 @@ done in the BIOS, or, on GNU/Linux, with the following command:
 Failure to do so will result in a library with poor performance.")
     (license license:bsd-3)))
 
+(define-public cglm
+  (package
+    (name "cglm")
+    (version "0.8.2")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/recp/cglm")
+             (commit (string-append "v" version))))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "1lcfl9ph4bnl3hckpx4hzwh8r4llnw94ik75igc5qy38wk468gmk"))))
+    (build-system cmake-build-system)
+    (arguments
+     `(#:configure-flags
+       (list "-DCGLM_USE_TEST=ON")))
+    (home-page "https://github.com/recp/cglm")
+    (synopsis "Mathematics C library for graphics programming")
+    (description
+     "@acronym{CGLM, C OpenGL Mathematics} is an optimised 3D maths library
+for graphics software based on the @acronym{GLSL, OpenGL Shading Language}
+specifications.
+
+It's similar to the original C++ GLM library but written in C99 and compatible
+with C89.")
+    (license license:expat)))
+
 (define-public glm
   (package
     (name "glm")
@@ -3961,7 +4414,7 @@ revised simplex and the branch-and-bound methods.")
 (define-public dealii
   (package
     (name "dealii")
-    (version "9.1.1")
+    (version "9.2.0")
     (source
      (origin
        (method url-fetch)
@@ -3969,7 +4422,7 @@ revised simplex and the branch-and-bound methods.")
                            "download/v" version "/dealii-" version ".tar.gz"))
        (sha256
         (base32
-         "0xhjv0gzswpjbc43xbrpwfc5848g508l01855nszx3g5gwzlhnzw"))
+         "0fm4xzrnb7dfn4415j24d8v3jkh0lssi86250x2f5wgi83xq4nnh"))
        (modules '((guix build utils)))
        (snippet
         ;; Remove bundled sources: UMFPACK, TBB, muParser, and boost
@@ -4116,7 +4569,7 @@ evaluates expressions using the standard order of operations.")
 (define-public xaos
   (package
     (name "xaos")
-    (version "4.0")
+    (version "4.2.1")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -4125,7 +4578,7 @@ evaluates expressions using the standard order of operations.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "00110p5xscjsmn7avfqgydn656zbmdj3l3y2fpv9b4ihzpid8n7a"))))
+                "0maw5am6rrkyjrprfg113zjq37mqj0iaznkg4h2927ff7wrprc94"))))
     (build-system gnu-build-system)
     (native-inputs `(("gettext" ,gettext-minimal)
                      ("qtbase" ,qtbase)
@@ -4148,12 +4601,14 @@ evaluates expressions using the standard order of operations.")
          (replace 'configure
            (lambda* (#:key outputs #:allow-other-keys)
              (let ((out (assoc-ref outputs "out")))
-               ;; The DESTDIR is originally set to install the xaos binary to
-               ;; the "bin" folder inside the build directory.  Setting make
-               ;; flags doesn't seem to change this.
                (substitute* "XaoS.pro"
+                 ;; The DESTDIR is originally set to install the xaos binary to
+                 ;; the "bin" folder inside the build directory.  Setting make
+                 ;; flags doesn't seem to change this.
                  (("DESTDIR.*$")
-                  (string-append "DESTDIR=" out "/bin")))
+                  (string-append "DESTDIR=" out "/bin"))
+                 ;; Set the correct path to the lrelease binary.
+                 (("lrelease-qt5") "lrelease"))
                (substitute* "src/include/config.h"
                  (("/usr/share/XaoS")
                   (string-append out "/share/XaoS")))
@@ -4190,7 +4645,7 @@ set.")
      (origin
        (method git-fetch)
        (uri (git-reference
-             (url "https://github.com/LLNL/hypre")
+             (url "https://github.com/hypre-space/hypre")
              (commit (string-append "v" version))))
        (file-name (git-file-name name version))
        (sha256
@@ -4276,7 +4731,8 @@ set.")
                            '("HYPRE_usr_manual"
                              "HYPRE_ref_manual")))
                #t))))))
-    (home-page "http://www.llnl.gov/casc/hypre/")
+    (home-page "https://computing.llnl.gov/projects\
+/hypre-scalable-linear-solvers-multigrid-methods")
     (synopsis "Library of solvers and preconditioners for linear equations")
     (description
      "HYPRE is a software library of high performance preconditioners and
@@ -4310,7 +4766,7 @@ structured and unstructured grid problems.")))
 (define-public matio
   (package
     (name "matio")
-    (version "1.5.6")
+    (version "1.5.19")
     (source
      (origin
        (method url-fetch)
@@ -4318,11 +4774,11 @@ structured and unstructured grid problems.")))
                            "matio-" version ".tar.gz"))
        (sha256
         (base32
-         "0y2qymgxank8wdiwc68ap8bxdzrhvyw86i29yh3xgn4z1njfd9ir"))))
+         "0vr8c1mz1k6mz0sgh6n3scl5c3a71iqmy5fnydrgq504icj4vym4"))))
     (build-system gnu-build-system)
     (inputs
      `(("zlib" ,zlib)
-       ("hdf5" ,hdf5)))
+       ("hdf5" ,hdf5-1.8)))
     (home-page "http://matio.sourceforge.net/")
     (synopsis "Library for reading and writing MAT files")
     (description "Matio is a library for reading and writing MAT files.  It
@@ -4487,7 +4943,7 @@ as equations, scalars, vectors, and matrices.")
 (define-public z3
   (package
     (name "z3")
-    (version "4.8.8")
+    (version "4.8.9")
     (home-page "https://github.com/Z3Prover/z3")
     (source (origin
               (method git-fetch)
@@ -4496,7 +4952,7 @@ as equations, scalars, vectors, and matrices.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1rn538ghqwxq0v8i6578j8mflk6fyv0cp4hjfqynzvinjbps56da"))))
+                "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
     (build-system gnu-build-system)
     (arguments
      `(#:imported-modules ((guix build python-build-system)
@@ -4609,7 +5065,7 @@ theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
                ;; Test scripts are generated, patch the shebang
                (("#!/bin/bash") (string-append "#!" (which "sh"))))
              #t)))))
-    (home-page "http://elpa.mpcdf.mpg.de")
+    (home-page "https://elpa.mpcdf.mpg.de")
     (synopsis "Eigenvalue solvers for symmetric matrices")
     (description
      "The ELPA library provides efficient and scalable direct eigensolvers for
@@ -4698,7 +5154,7 @@ reduction.")
 (define-public mcrl2
   (package
     (name "mcrl2")
-    (version "201908.0")
+    (version "202006.0")
     (source (origin
               (method url-fetch)
               (uri (string-append
@@ -4706,7 +5162,7 @@ reduction.")
                     version ".tar.gz"))
               (sha256
                (base32
-                "1i4xgl2d5fgiz1mwi50cyfkrrcpm8nxfayfjgmhq7chs58wlhfsz"))))
+                "167ryrzk1a2j53c2j198jlxa98amcaym070gkcj730619gymv5zl"))))
     (inputs
      `(("boost" ,boost)
        ("glu" ,glu)
@@ -4754,6 +5210,58 @@ be fed to @command{tcalc} through the command line.")
   (home-page "https://sites.google.com/site/mohammedisam2000/tcalc")
   (license license:gpl3+)))
 
+(define-public tiny-bignum
+  (let ((commit "1d7a1f9b8e77316187a6b3eae8e68d60a6f9a4d4"))
+    (package
+     (name "tiny-bignum")
+     (version (git-version "0" "0" commit))
+     (source
+      (origin
+        (method git-fetch)
+        (uri (git-reference
+              (url "https://github.com/kokke/tiny-bignum-c")
+              (commit commit)))
+        (file-name (git-file-name "tiny-bignum" commit))
+        (sha256
+         (base32 "0vj71qlhlaa7d92bfar1kwqv6582dqrby8x3kdw0yzh82k2023g6"))))
+     (build-system gnu-build-system)
+     (arguments
+      `(#:phases
+        (modify-phases %standard-phases
+          (delete 'configure)
+          (add-after 'unpack 'patch-tests
+            (lambda _
+              (substitute* "scripts/test_rand.py"
+                (("\t") "  ")
+                (("\" % (\\w+)" _ symbol) (string-append "\" % int(" symbol ")")))
+              #t))
+          (replace 'check
+            (lambda* (#:key tests? #:allow-other-keys)
+              (when tests?
+                (invoke "make" "test"))
+              #t))
+          (replace 'install
+            (lambda* (#:key outputs #:allow-other-keys)
+              (let ((share (string-append (assoc-ref outputs "out") "/share"))
+                    (doc (string-append (assoc-ref outputs "out") "/doc")))
+                (mkdir-p share)
+                (install-file "bn.c" share)
+                (install-file "bn.h" share)
+                (mkdir-p doc)
+                (install-file "LICENSE" doc)
+                (install-file "README.md" doc))
+              #t)))))
+     (native-inputs
+      `(("python" ,python-wrapper)))
+     (home-page "https://github.com/kokke/tiny-bignum-c")
+     (synopsis "Small portable multiple-precision unsigned integer arithmetic in C")
+     (description
+      "This library provides portable Arbitrary-precision unsigned integer
+arithmetic in C, for calculating with large numbers.  Basic arithmetic (+, -,
+*, /, %) and bitwise operations (&, |, ^. <<, >>) plus increments, decrements
+and comparisons are supported.")
+     (license license:unlicense))))
+
 (define-public sundials
   (package
     (name "sundials")
@@ -5551,10 +6059,10 @@ compiled against the nauty library.")
          "1j5aji1g2vmdvc0gqz45n2ll2l2f6czca04wiyfl5g3sm3a6vhvb"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("m4"m4)))
+     `(("m4" ,m4)))
     (inputs
      `(("glpk" ,glpk)
-       ("gmp"gmp)))
+       ("gmp" ,gmp)))
     (home-page "https://www.bugseng.com/parma-polyhedra-library")
     (synopsis
      "Parma Polyhedra Library for computations with polyhedra")
@@ -5650,7 +6158,7 @@ researchers and developers alike to get started on SAT.")
 (define-public libqalculate
   (package
     (name "libqalculate")
-    (version "3.8.0")
+    (version "3.19.0")
     (source
      (origin
        (method git-fetch)
@@ -5659,7 +6167,7 @@ researchers and developers alike to get started on SAT.")
              (commit (string-append "v" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1vbaza9c7159xf2ym90l0xkyj2mp6c3hbghhsqn29yvz08fda9df"))
+        (base32 "1w44407wb552q21dz4m2nwwdi8b9hzjb2w1l3ffsikzqckc7wbyj"))
        (patches
         (search-patches "libqalculate-3.8.0-libcurl-ssl-fix.patch"))))
     (build-system gnu-build-system)
@@ -5757,3 +6265,140 @@ and conversions, physical constants, symbolic calculations (including
 integrals and equations), arbitrary precision, uncertainty propagation,
 interval arithmetic, plotting.")
     (license license:gpl2+)))
+
+(define-public numdiff
+  (package
+    (name "numdiff")
+    (version "5.9.0")
+    (source
+     (origin
+       (method url-fetch)
+       (uri (string-append "mirror://savannah/numdiff/numdiff-"
+                           version ".tar.gz"))
+       (sha256
+        (base32
+         "1vzmjh8mhwwysn4x4m2vif7q2k8i19x8azq7pzmkwwj4g48lla47"))))
+    (build-system gnu-build-system)
+    (arguments
+     '(#:tests? #f ; There are no tests.
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'compress-documentation 'delete-precompressed-info-file
+           (lambda _
+             (delete-file (string-append (assoc-ref %outputs "out")
+                                         "/share/info/numdiff.info.gz"))
+             #t)))))
+    (home-page "https://nongnu.org/numdiff/")
+    (synopsis "Compare files with numeric fields")
+    (description
+     "Numdiff compares files line by line and field by field, ignoring small
+numeric differences and differences in numeric formats.")
+    (license license:gpl3+)))
+
+(define-public why3
+  (package
+    (name "why3")
+    (version "1.3.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
+                                  "/38291/why3-" version ".tar.gz"))
+              (sha256
+               (base32
+                "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv"))))
+    (build-system ocaml-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("which" ,which)))
+    (propagated-inputs
+     `(("camlzip" ,camlzip)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-menhir" ,ocaml-menhir)
+       ("ocaml-num" ,ocaml-num)
+       ("ocaml-zarith" ,ocaml-zarith)))
+    (inputs
+     `(("coq-flocq" ,coq-flocq)
+       ("emacs-minimal" ,emacs-minimal)
+       ("zlib" ,zlib)))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-configure
+           (lambda _
+             (setenv "CONFIG_SHELL" (which "sh"))
+             (substitute* "configure"
+               ;; find ocaml-num in the correct directory
+               (("\\$DIR/nums.cma") "$DIR/../nums.cma")
+               (("\\$DIR/num.cmi") "$DIR/../num.cmi"))
+             #t))
+         (add-after 'configure 'fix-makefile
+           (lambda _
+             (substitute* "Makefile"
+               ;; find ocaml-num in the correct directory
+               (("site-lib/num") "site-lib"))
+             #t))
+        (add-after 'install 'install-lib
+          (lambda _
+            (invoke "make" "byte")
+            (invoke "make" "install-lib")
+            #t)))))
+    (home-page "http://why3.lri.fr")
+    (synopsis "Deductive program verification")
+    (description "Why3 provides a language for specification and programming,
+called WhyML, and relies on external theorem provers, both automated and
+interactive, to discharge verification conditions.  Why3 comes with a standard
+library of logical theories (integer and real arithmetic, Boolean operations,
+sets and maps, etc.) and basic programming data structures (arrays, queues,
+hash tables, etc.).  A user can write WhyML programs directly and get
+correct-by-construction OCaml programs through an automated extraction
+mechanism.  WhyML is also used as an intermediate language for the verification
+of C, Java, or Ada programs.")
+    (license license:lgpl2.1)))
+
+(define-public frama-c
+  (package
+    (name "frama-c")
+    (version "22.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://frama-c.com/download/frama-c-"
+                                  version "-Titanium.tar.gz"))
+              (sha256
+               (base32
+                "1mq1fijka95ydrla486yr4w6wdl9l7vmp512s1q00b0p6lmfwmkh"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:tests? #f; no test target in Makefile
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'export-shell
+           (lambda* (#:key inputs #:allow-other-keys)
+             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
+                                                   "/bin/sh"))
+             #t)))))
+    (inputs
+     `(("gmp" ,gmp)))
+    (propagated-inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-easy-format" ,ocaml-easy-format)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-yojson" ,ocaml-yojson)
+       ("ocaml-zarith" ,ocaml-zarith)
+       ("why3" ,why3)))
+    (native-search-paths
+     (list (search-path-specification
+            (variable "FRAMAC_SHARE")
+            (files '("share/frama-c"))
+            (separator #f))
+           (search-path-specification
+            (variable "FRAMAC_LIB")
+            (files '("lib/frama-c"))
+            (separator #f))))
+    (home-page "http://frama-c.com")
+    (synopsis "C source code analysis platform")
+    (description "Frama-C is an extensible and collaborative platform dedicated
+to source-code analysis of C software.  The Frama-C analyzers assist you in
+various source-code-related activities, from the navigation through unfamiliar
+projects up to the certification of critical software.")
+    (license license:lgpl2.1+)))