gnu: Add r-geosphere.
[jackhill/guix/guix.git] / gnu / packages / maths.scm
index f0b3bf2..f9e5d2c 100644 (file)
@@ -2,17 +2,17 @@
 ;;; Copyright © 2013, 2014, 2015, 2016 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 Eric Bavier <bavier@member.fsf.org>
+;;; Copyright © 2014, 2015, 2016, 2017, 2018 Eric Bavier <bavier@member.fsf.org>
 ;;; Copyright © 2014 Federico Beffa <beffa@fbengineering.ch>
 ;;; Copyright © 2014 Mathieu Lirzin <mathieu.lirzin@openmailbox.org>
-;;; Copyright © 2015, 2016, 2017 Ricardo Wurmus <rekado@elephly.net>
+;;; Copyright © 2015, 2016, 2017, 2018 Ricardo Wurmus <rekado@elephly.net>
 ;;; Copyright © 2015 Sou Bunnbu <iyzsong@gmail.com>
 ;;; Copyright © 2015 Mark H Weaver <mhw@netris.org>
-;;; Copyright © 2015, 2016, 2017 Efraim Flashner <efraim@flashner.co.il>
+;;; Copyright © 2015, 2016, 2017, 2018 Efraim Flashner <efraim@flashner.co.il>
 ;;; Copyright © 2015 Fabian Harfert <fhmgufs@web.de>
 ;;; Copyright © 2016 Roel Janssen <roel@gnu.org>
 ;;; Copyright © 2016 Kei Kebreau <kkebreau@posteo.net>
-;;; Copyright © 2016, 2017 Ludovic Courtès <ludo@gnu.org>
+;;; Copyright © 2016, 2017, 2018 Ludovic Courtès <ludo@gnu.org>
 ;;; Copyright © 2016 Leo Famulari <leo@famulari.name>
 ;;; Copyright © 2016, 2017 Thomas Danckaert <post@thomasdanckaert.be>
 ;;; Copyright © 2017 Paul Garlick <pgarlick@tourbillion-technology.com>
@@ -20,6 +20,9 @@
 ;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
 ;;; Copyright © 2017 Theodoros Foradis <theodoros@foradis.org>
 ;;; Copyright © 2017 Arun Isaac <arunisaac@systemreboot.net>
+;;; Copyright © 2017, 2018 Tobias Geerinckx-Rice <me@tobias.gr>
+;;; Copyright © 2017 Dave Love <me@fx@gnu.org>
+;;; Copyright © 2018 Jan Nieuwenhuizen <janneke@gnu.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -90,6 +93,8 @@
   #:use-module (gnu packages perl)
   #:use-module (gnu packages pkg-config)
   #:use-module (gnu packages python)
+  #:use-module (gnu packages python-web)
+  #:use-module (gnu packages qt)
   #:use-module (gnu packages readline)
   #:use-module (gnu packages tbb)
   #:use-module (gnu packages scheme)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages tex)
   #:use-module (gnu packages tls)
+  #:use-module (gnu packages version-control)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
   #:use-module (srfi srfi-1))
@@ -151,14 +157,14 @@ interactive dialogs to guide them.")
 (define-public coda
   (package
     (name "coda")
-    (version "2.18.2")
+    (version "2.18.3")
     (source
      (origin
        (method url-fetch)
        (uri (string-append "https://github.com/stcorp/coda/releases/download/"
                            version "/coda-" version ".tar.gz"))
        (sha256
-        (base32 "01fnqcby9jijvf3jxr1fk4bny059lvvq5wbqm7ns60ilykfdnm6a"))
+        (base32 "1zlzgcvwmmjm8mw8w4rg2rqy0pjilz7kyyxm0y4p8cbljbbjxxz0"))
        (patches (search-patches "coda-use-system-libs.patch"))
        (modules '((guix build utils)))
        (snippet
@@ -200,6 +206,20 @@ programming languages.")
             (sha256 (base32
                      "11hnp3gcmcc5kci2caxw4hs6m08h2mhqs3xzqq7iafx1ha2ggwyw"))))
    (build-system gnu-build-system)
+   (inputs
+    `(("readline" ,readline)
+      ("python" ,python-wrapper)        ;for 'units_cur' script
+      ("python-requests" ,python-requests)))
+   (arguments
+    `(#:phases (modify-phases %standard-phases
+                 (add-after 'install 'wrap-units_cur
+                   (lambda* (#:key outputs #:allow-other-keys)
+                     (let* ((out (assoc-ref outputs "out"))
+                            (bin (string-append out "/bin")))
+                       (wrap-program (string-append bin "/units_cur")
+                         `("PYTHONPATH" ":" prefix
+                           ,(search-path-as-string->list (getenv "PYTHONPATH"))))
+                       #t))))))
    (synopsis "Conversion between thousands of scales")
    (description
     "GNU Units converts numeric quantities between units of measure.  It
@@ -239,14 +259,14 @@ routines that have been extracted from the V8 JavaScript engine.")
 (define-public dionysus
   (package
     (name "dionysus")
-    (version "1.3.0")
+    (version "1.4.0")
     (source (origin
               (method url-fetch)
               (uri (string-append "mirror://gnu/dionysus/dionysus-" version
-                                  ".tar.gz"))
+                                  ".tar.xz"))
               (sha256
                (base32
-                "1aqnvw6z33bzqgd1ga571pnx6vq2zrkckm1cz91grv45h4jr9vgs"))))
+                "194pzs1mlsj4ww6v37qq3961h5hckm5h805cv0r14xj3g9wfx2sk"))))
     (build-system gnu-build-system)
     (inputs `(("tcl" ,tcl)))                      ;for 'tclsh'
     (synopsis "Local search for universal constants and scientific values")
@@ -319,7 +339,7 @@ the OCaml language.")
 (define-public glpk
   (package
     (name "glpk")
-    (version "4.63")
+    (version "4.65")
     (source
      (origin
       (method url-fetch)
@@ -327,7 +347,7 @@ the OCaml language.")
                           version ".tar.gz"))
       (sha256
        (base32
-        "1xp7nclmp8inp20968bvvfcwmz3mz03sbm0v3yjz8aqwlpqjfkci"))))
+        "040sfaa9jclg2nqdh83w71sv9rc1sznpnfiripjdyr48cady50a2"))))
     (build-system gnu-build-system)
     (inputs
      `(("gmp" ,gmp)))
@@ -398,18 +418,26 @@ computing convex hulls.")
 (define-public arpack-ng
   (package
     (name "arpack-ng")
-    (version "3.2.0")
+    (version "3.5.0")
+    (home-page "https://github.com/opencollab/arpack-ng")
     (source
      (origin
        (method url-fetch)
-       (uri (string-append "https://github.com/opencollab/arpack-ng/archive/"
-                           version ".tar.gz"))
+       (uri (string-append home-page "/archive/" version ".tar.gz"))
        (file-name (string-append name "-" version ".tar.gz"))
        (sha256
         (base32
-         "1fwch6vipms1ispzg2djvbzv5wag36f1dmmr3xs3mbp6imfyhvff"))))
+         "0f8jx3fifmj9qdp289zr7r651y1q48k1jya859rqxq62mvis7xsh"))))
     (build-system gnu-build-system)
-    (home-page "https://github.com/opencollab/arpack-ng")
+    (arguments
+     '(#:phases (modify-phases %standard-phases
+                  (add-after 'unpack 'autoreconf
+                    (lambda _
+                      (invoke "autoreconf" "-vfi"))))))
+    (native-inputs
+     `(("autoconf" ,autoconf)
+       ("automake" ,automake)
+       ("libtool" ,libtool)))
     (inputs
      `(("lapack" ,lapack)
        ("fortran" ,gfortran)))
@@ -420,6 +448,21 @@ large scale eigenvalue problems.")
     (license (license:non-copyleft "file://COPYING"
                                 "See COPYING in the distribution."))))
 
+(define-public arpack-ng-3.3.0
+  (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"))
+       (sha256
+        (base32
+         "1cz53wqzcf6czmcpfb3vb61xi0rn5bwhinczl65hpmbrglg82ndd"))))))
+
 (define-public arpack-ng-openmpi
   (package (inherit arpack-ng)
     (name "arpack-ng-openmpi")
@@ -447,12 +490,6 @@ large scale eigenvalue problems.")
               ("python" ,python-2)))
     (arguments
      `(#:configure-flags (list
-                          ;; Install to PREFIX/lib (the default is
-                          ;; PREFIX/lib64).
-                          (string-append "-DCMAKE_INSTALL_LIBDIR="
-                                         (assoc-ref %outputs "out")
-                                         "/lib")
-
                           "-DBUILD_SHARED_LIBS:BOOL=YES"
                           "-DLAPACKE=ON"
 
@@ -684,7 +721,9 @@ incompatible with HDF5.")
        #:configure-flags '("--enable-cxx"
                            "--enable-fortran"
                            "--enable-fortran2003")
-
+       ;; Use -fPIC to allow the R bindings to link with the static libraries
+       #:make-flags (list "CFLAGS=-fPIC"
+                          "CXXFLAGS=-fPIC")
        #:phases
        (modify-phases %standard-phases
          (add-before 'configure 'patch-configure
@@ -708,7 +747,11 @@ incompatible with HDF5.")
              ;; unnecessary store references to those compilers:
              (substitute* "src/libhdf5.settings"
               (("(/gnu/store/)([a-Z0-9]*)" all prefix hash)
-               (string-append prefix (string-take hash 10) "...")))
+               (string-append prefix (string-take hash 10) "..."))
+              ;; Don't record the build-time kernel version to make the
+              ;; settings file reproducible.
+              (("Uname information:.*")
+               "Uname information: Linux\n"))
              #t))
          (add-after 'install 'patch-references
            (lambda* (#:key inputs outputs #:allow-other-keys)
@@ -1214,7 +1257,7 @@ interfaces.")
 (define-public ceres
   (package
     (name "ceres-solver")
-    (version "1.11.0")
+    (version "1.13.0")
     (home-page "http://ceres-solver.org/")
     (source (origin
               (method url-fetch)
@@ -1222,7 +1265,7 @@ interfaces.")
                                   version ".tar.gz"))
               (sha256
                (base32
-                "0i7qkbf8g6pd8arxzldppga26ckv93y8zldsfz6wbd4n6b1nqrjd"))))
+                "1kbxgab3q1vgyq7hjqasr1lji4b2sgn7ss351amklkb3jyhr1x0x"))))
     (build-system cmake-build-system)
     (arguments
      ;; TODO: Build HTML user documentation and install separately.
@@ -1344,6 +1387,7 @@ script files.")
                "https://github.com/tpaviot/oce/archive/OCE-"
                version
                ".tar.gz"))
+        (patches (search-patches "opencascade-oce-glibc-2.26.patch"))
         (sha256
           (base32
             "0vpmnb0k5y2f7lpmwx9pg9yfq24zjvnsak5alzacncfm1hv9b6cd"))))
@@ -1593,7 +1637,7 @@ scientific applications modeled by partial differential equations.")
 (define-public slepc
   (package
     (name "slepc")
-    (version "3.8.0")
+    (version "3.8.2")
     (source
      (origin
        (method url-fetch)
@@ -1601,7 +1645,7 @@ scientific applications modeled by partial differential equations.")
                            version ".tar.gz"))
        (sha256
         (base32
-         "0qyrsdndfdw2g0jmj9iskxj3j20zlkplhv26288s079dhm7cr365"))))
+         "04zd48p43rnvg68p6cp28zll0px5whglc5v0sc3s6vdj1v920z8y"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("python" ,python-2)))
@@ -1630,7 +1674,7 @@ scientific applications modeled by partial differential equations.")
               (format #t "configure flags: ~s~%" flags)
               (setenv "SLEPC_DIR" (getcwd))
               (setenv "PETSC_DIR" (assoc-ref inputs "petsc"))
-              (zero? (apply system* "./configure" flags)))))
+              (apply invoke "./configure" flags))))
          (add-after 'install 'delete-doc
           ;; TODO: SLEPc installs HTML documentation alongside headers in
           ;; $out/include.  We'd like to move them to share/doc, but delete
@@ -1659,7 +1703,7 @@ as well as other related problems such as the singular value decomposition.
 The emphasis of the software is on methods and techniques appropriate for
 problems in which the associated matrices are sparse, for example, those
 arising after the discretization of partial differential equations.")
-    (license license:lgpl3)))
+    (license license:bsd-2)))
 
 (define-public slepc-complex
   (package (inherit slepc)
@@ -1868,7 +1912,7 @@ sparse system of linear equations A x = b using Guassian elimination.")
     (build-system r-build-system)
     (native-inputs
      `(("gfortran" ,gfortran)))
-    (home-page "http://cran.r-project.org/web/packages/quadprog")
+    (home-page "https://cran.r-project.org/web/packages/quadprog")
     (synopsis "Functions to solve quadratic programming problems")
     (description
      "This package contains routines and documentation for solving quadratic
@@ -1878,16 +1922,16 @@ programming problems.")
 (define-public r-pracma
   (package
     (name "r-pracma")
-    (version "2.0.7")
+    (version "2.1.4")
     (source (origin
       (method url-fetch)
       (uri (cran-uri "pracma" version))
       (sha256
-        (base32 "0hxa0rbbp54j0c05qj7vfwhqfdmiz5ax8vhqxd09g33x7c0hqbc5"))))
+        (base32 "1ygm81i7mqvh229dp9935djjyb120p3bqvaf4k572sa4q63fzjhc"))))
     (build-system r-build-system)
     (propagated-inputs
      `(("r-quadprog" ,r-quadprog)))
-    (home-page "http://cran.r-project.org/web/packages/pracma")
+    (home-page "https://cran.r-project.org/web/packages/pracma")
     (synopsis "Practical numerical math functions")
     (description "This package provides functions for numerical analysis and
 linear algebra, numerical optimization, differential equations, plus some
@@ -1946,8 +1990,7 @@ void mc64ad_ (int *a, int *b, int *c, int *d, int *e, double *f, int *g,
     (arguments
      `(#:configure-flags '("-Denable_blaslib:BOOL=NO" ;do not use internal cblas
                            "-DTPL_BLAS_LIBRARIES=openblas"
-                           "-DBUILD_SHARED_LIBS:BOOL=YES"
-                           "-DCMAKE_INSTALL_LIBDIR=lib")))
+                           "-DBUILD_SHARED_LIBS:BOOL=YES")))
     (home-page "http://crd-legacy.lbl.gov/~xiaoye/SuperLU/")
     (synopsis "Supernodal direct solver for sparse linear systems")
     (description
@@ -2473,7 +2516,7 @@ point numbers.")
 (define-public wxmaxima
   (package
     (name "wxmaxima")
-    (version "17.05.1")
+    (version "18.02.0")
     (source
      (origin
        (method url-fetch)
@@ -2482,12 +2525,12 @@ point numbers.")
        (file-name (string-append name "-" version ".tar.gz"))
        (sha256
         (base32
-         "0dv0cy0cf46v0cbw32izscpkdmpxg1qhwq1f4cz46kkqd8k4yfbj"))))
-    (build-system gnu-build-system)
+         "03kr2rgfp4hcf3is8m8d8f9hj660c3xgrc50vrrfpixx4syh6wvj"))
+       (patches
+        (search-patches "wxmaxima-do-not-use-old-gnuplot-parameters.patch"))))
+    (build-system cmake-build-system)
     (native-inputs
-     `(("autoconf" ,autoconf)
-       ("automake" ,automake)
-       ("gettext" ,gettext-minimal)))
+     `(("gettext" ,gettext-minimal)))
     (inputs
      `(("wxwidgets" ,wxwidgets)
        ("maxima" ,maxima)
@@ -2496,11 +2539,9 @@ point numbers.")
        ("gtk+" ,gtk+)
        ("shared-mime-info" ,shared-mime-info)))
     (arguments
-     `(#:phases
+     `(#:tests? #f ; no check target
+       #:phases
        (modify-phases %standard-phases
-         (add-after 'unpack 'autoconf
-           (lambda _
-             (zero? (system* "sh" "bootstrap"))))
          (add-after 'install 'wrap-program
            (lambda* (#:key inputs outputs #:allow-other-keys)
              (wrap-program (string-append (assoc-ref outputs "out")
@@ -2600,7 +2641,7 @@ parts of it.")
 (define-public openblas
   (package
     (name "openblas")
-    (version "0.2.19")
+    (version "0.2.20")
     (source
      (origin
        (method url-fetch)
@@ -2609,10 +2650,10 @@ parts of it.")
        (file-name (string-append name "-" version ".tar.gz"))
        (sha256
         (base32
-         "071zqnmnxhh0c9phzyn3f198yxa0hjxda7016azdbq2056sm70w7"))))
+         "1bd03c5xni0bla0wg1wba841b36b0sg13sjja955kn5xzvy4i61a"))))
     (build-system gnu-build-system)
     (arguments
-     `(#:tests? #f  ;no "check" target
+     `(#:test-target "test"
        ;; DYNAMIC_ARCH is only supported on x86.  When it is disabled and no
        ;; TARGET is specified, OpenBLAS will tune itself to the build host, so
        ;; we need to disable substitutions.
@@ -2625,7 +2666,6 @@ parts of it.")
        #:make-flags
        (list (string-append "PREFIX=" (assoc-ref %outputs "out"))
              "SHELL=bash"
-             "NO_LAPACK=1"
              ;; Build the library for all supported CPUs.  This allows
              ;; switching CPU targets at runtime with the environment variable
              ;; OPENBLAS_CORETYPE=<type>, where "type" is a supported CPU type.
@@ -2646,11 +2686,21 @@ parts of it.")
                    '("TARGET=ARMV8"))
                   (else '()))))
        ;; no configure script
-       #:phases (alist-delete 'configure %standard-phases)))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure)
+         (add-before 'build 'set-extralib
+           (lambda* (#:key inputs #:allow-other-keys)
+             ;; Get libgfortran found when building in utest.
+             (setenv "FEXTRALIB"
+                     (string-append "-L" (assoc-ref inputs "fortran-lib")
+                                    "/lib"))
+             #t)))))
     (inputs
-     `(("fortran" ,gfortran)))
+     `(("fortran-lib" ,gfortran "lib")))
     (native-inputs
      `(("cunit" ,cunit)
+       ("fortran" ,gfortran)
        ("perl" ,perl)))
     (home-page "http://www.openblas.net/")
     (synopsis "Optimized BLAS library based on GotoBLAS")
@@ -2786,7 +2836,7 @@ environments.")
 (define-public openspecfun
   (package
     (name "openspecfun")
-    (version "0.5.2")
+    (version "0.5.3")
     (source
      (origin
        (method url-fetch)
@@ -2795,14 +2845,15 @@ environments.")
        (file-name (string-append name "-" version ".tar.gz"))
        (sha256
         (base32
-         "1y5b2h6f2k72536kym3vzy3li3bhpd23x463g7hdmjdi3cncavz1"))))
+         "1rs1bv8jq751fv9vq79890wqf9xlbjc7lvz3ighzyfczbyjcf18m"))))
     (build-system gnu-build-system)
     (arguments
-     '(#:tests? #f  ;no "check" target
+     '(#:tests? #f                      ; no "check" target
        #:make-flags
        (list (string-append "prefix=" (assoc-ref %outputs "out")))
-       ;; no configure script
-       #:phases (modify-phases %standard-phases (delete 'configure))))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure))))         ; no configure script
     (inputs
      `(("fortran" ,gfortran)))
     (home-page "https://github.com/JuliaLang/openspecfun")
@@ -3021,7 +3072,7 @@ specifications.")
 (define-public lpsolve
   (package
     (name "lpsolve")
-    (version "5.5.2.0")
+    (version "5.5.2.5")
     (source
      (origin
       (method url-fetch)
@@ -3029,7 +3080,7 @@ specifications.")
                           "/lp_solve_" version "_source.tar.gz"))
       (sha256
        (base32
-        "176c7f023mb6b8bfmv4rfqnrlw88lsg422ca74zjh19i2h5s69sq"))
+        "12pj1idjz31r7c2mb5w03vy1cmvycvbkx9z29s40qdmkp1i7q6i0"))
       (modules '((guix build utils)))
       (snippet
        '(substitute* (list "lp_solve/ccc" "lpsolve55/ccc")
@@ -3047,16 +3098,17 @@ specifications.")
           (("isnan\\(0\\)") "isnan(0.)")))))
     (build-system gnu-build-system)
     (arguments
-     `(#:tests? #f ; no check target
+     `(#:tests? #f                      ; no check target
        #:phases
        (modify-phases %standard-phases
-         (delete 'configure)
+         (delete 'configure)            ; no configure script
          (replace 'build
            (lambda _
-             (and (with-directory-excursion "lpsolve55"
-                    (zero? (system* "bash" "ccc")))
-                  (with-directory-excursion "lp_solve"
-                    (zero? (system* "bash" "ccc"))))))
+             (with-directory-excursion "lpsolve55"
+               (invoke "bash" "ccc"))
+             (with-directory-excursion "lp_solve"
+               (invoke "bash" "ccc"))
+             #t))
          (replace 'install
            (lambda* (#:key outputs #:allow-other-keys)
              (let* ((out (assoc-ref outputs "out"))
@@ -3065,11 +3117,8 @@ specifications.")
                     ;; This is where LibreOffice expects to find the header
                     ;; files, and where they are installed by Debian.
                     (include (string-append out "/include/lpsolve")))
-               (mkdir-p lib)
-               (copy-file "lpsolve55/bin/ux64/liblpsolve55.a"
-                          (string-append lib "/liblpsolve55.a"))
-               (copy-file "lpsolve55/bin/ux64/liblpsolve55.so"
-                          (string-append lib "/liblpsolve55.so"))
+               (install-file "lpsolve55/bin/ux64/liblpsolve55.a" lib)
+               (install-file "lpsolve55/bin/ux64/liblpsolve55.so" lib)
                (install-file "lp_solve/bin/ux64/lp_solve" bin)
 
                ;; Install a subset of the header files as on Debian
@@ -3411,14 +3460,14 @@ supports compressed MAT files, as well as newer (version 7.3) MAT files.")
 (define-public vc
   (package
     (name "vc")
-    (version "1.2.0")
+    (version "1.3.3")
     (source
       (origin (method url-fetch)
               (uri (string-append "https://github.com/VcDevel/Vc/releases/"
                                   "download/" version "/Vc-" version ".tar.gz"))
               (sha256
                (base32
-                "1rh6dhqar3y07n4xqyml0sa0v48qv3ch9dc3yc2in855hlh4vnqi"))))
+                "1zmlpn32jzb38smp3j834llmbix3whsrbw0h397qxysbw792kih8"))))
     (build-system cmake-build-system)
     (arguments
      '(#:configure-flags
@@ -3555,11 +3604,7 @@ as equations, scalars, vectors, and matrices.")
              "-DINSTALL_PYTHON_BINDINGS=true"
              (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR="
                             %output
-                            "/lib/python2.7/site-packages")
-             (string-append "-DCMAKE_INSTALL_LIBDIR="
-                            %output
-                            "/lib"))
-
+                            "/lib/python2.7/site-packages"))
        #:phases
        (modify-phases %standard-phases
          (add-before 'configure 'bootstrap
@@ -3619,9 +3664,93 @@ theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
                (("\\\\n") "")))))))
     (home-page "http://cubicle.lri.fr/")
     (synopsis "Model checker for array-based systems")
-    (description "Cubicle is an open source model checker for verifying safety
-properties of array-based systems.  This is a syntactically restricted class of
-parametrized transition systems with states represented as arrays indexed by an
-arbitrary number of processes.  Cache coherence protocols and mutual exclusion
-algorithms are typical examples of such systems.")
+    (description "Cubicle is a model checker for verifying safety properties
+of array-based systems.  This is a syntactically restricted class of
+parametrized transition systems with states represented as arrays indexed by
+an arbitrary number of processes.  Cache coherence protocols and mutual
+exclusion algorithms are typical examples of such systems.")
     (license license:asl2.0)))
+
+(define-public elemental
+  (package
+    (name "elemental")
+    (version "0.87.7")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://github.com/elemental/Elemental/"
+                                  "archive/v" version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "1nfp82w22pi8x8fg9sc37z8kf84dqi1dhxp8bbk7571y4aygvv3v"))))
+    (build-system cmake-build-system)
+    (home-page "http://libelemental.org")
+    (native-inputs
+     `(("gfortran" ,gfortran)))
+    (inputs
+     `(("blas" ,openblas)
+       ("gfortran:lib" ,gfortran "lib")
+       ("gmp" ,gmp)
+       ("lapack" ,lapack)
+       ("metis" ,metis)
+       ("mpc" ,mpc)
+       ("mpfr" ,mpfr)
+       ("mpi" ,openmpi)
+       ("qd" ,qd)))
+    (arguments
+     `(#:build-type "Release"           ;default RelWithDebInfo not supported
+       #:configure-flags `("-DEL_DISABLE_PARMETIS:BOOL=YES"
+                           "-DEL_AVOID_COMPLEX_MPI:BOOL=NO"
+                           "-DEL_CACHE_WARNINGS:BOOL=YES"
+                           "-DEL_TESTS:BOOL=YES"
+                           "-DCMAKE_INSTALL_LIBDIR=lib"
+                           "-DGFORTRAN_LIB=gfortran")
+       #:phases (modify-phases %standard-phases
+                  (add-before 'check 'setup-tests
+                    (lambda _
+                      ;; Parallelism is done at the MPI layer.
+                      (setenv "OMP_NUM_THREADS" "1")
+                      #t))
+                  (add-after 'install 'remove-tests
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      ;; Tests are installed, with no easy configuration
+                      ;; switch to prevent this, so delete them.
+                      (delete-file-recursively
+                       (string-append (assoc-ref outputs "out") "/bin"))
+                      #t)))))
+    (synopsis "Dense and sparse-direct linear algebra and optimization")
+    (description "Elemental is a modern C++ library for distributed-memory
+dense and sparse-direct linear algebra, conic optimization, and lattice
+reduction.")
+    (license license:bsd-2)))
+
+(define-public mcrl2
+  (package
+    (name "mcrl2")
+    (version "201707.1.15162")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://www.mcrl2.org/download/devel/mcrl2-"
+                                  version
+                                  ".tar.gz"))
+              (sha256
+               (base32
+                "1ziww2fchsklm25hl9p2mngssxfh9w07nc114cncqaxfibqp2p8f"))))
+    (native-inputs
+     `(("subversion" ,subversion)))
+    (inputs
+     `(("boost" ,boost)
+       ("glu" ,glu)
+       ("mesa" ,mesa)
+       ("qt" ,qt)))
+    (build-system cmake-build-system)
+    (synopsis "Toolset for the mCRL2 formal specification language")
+    (description
+     "@dfn{mCRL2} (micro Common Representation Language 2) is a formal
+specification language for describing concurrent discrete event systems.  Its
+toolset supports analysis and automatic verification, linearisation, simulation,
+state-space exploration and generation, and tools to optimise and analyse
+specifications.  Also, state spaces can be manipulated, visualised and
+analysed.")
+    (home-page "http://mcrl2.org")
+    (license license:boost1.0)))