gnu: suitesparse: Use modify-phases.
[jackhill/guix/guix.git] / gnu / packages / maths.scm
index fc98eae..5f2697e 100644 (file)
@@ -1,20 +1,24 @@
 ;;; GNU Guix --- Functional package management for GNU
 ;;; Copyright © 2013, 2014, 2015, 2016 Andreas Enge <andreas@enge.fr>
 ;;; Copyright © 2013 Nikita Karetnikov <nikita@karetnikov.org>
-;;; Copyright © 2014, 2016 John Darrington <jmd@gnu.org>
-;;; Copyright © 2014, 2015, 2016 Eric Bavier <bavier@member.fsf.org>
+;;; Copyright © 2014, 2016, 2017 John Darrington <jmd@gnu.org>
+;;; Copyright © 2014, 2015, 2016, 2017 Eric Bavier <bavier@member.fsf.org>
 ;;; Copyright © 2014 Federico Beffa <beffa@fbengineering.ch>
 ;;; Copyright © 2014 Mathieu Lirzin <mathieu.lirzin@openmailbox.org>
-;;; Copyright © 2015, 2016 Ricardo Wurmus <rekado@elephly.net>
+;;; Copyright © 2015, 2016, 2017 Ricardo Wurmus <rekado@elephly.net>
 ;;; Copyright © 2015 Sou Bunnbu <iyzsong@gmail.com>
 ;;; Copyright © 2015 Mark H Weaver <mhw@netris.org>
-;;; Copyright © 2015, 2016 Efraim Flashner <efraim@flashner.co.il>
+;;; Copyright © 2015, 2016, 2017 Efraim Flashner <efraim@flashner.co.il>
 ;;; Copyright © 2015 Fabian Harfert <fhmgufs@web.de>
 ;;; Copyright © 2016 Roel Janssen <roel@gnu.org>
 ;;; Copyright © 2016 Kei Kebreau <kei@openmailbox.org>
-;;; Copyright © 2016 Ludovic Courtès <ludo@gnu.org>
+;;; Copyright © 2016, 2017 Ludovic Courtès <ludo@gnu.org>
 ;;; Copyright © 2016 Leo Famulari <leo@famulari.name>
 ;;; Copyright © 2016 Thomas Danckaert <post@thomasdanckaert.be>
+;;; Copyright © 2017 Paul Garlick <pgarlick@tourbillion-technology.com>
+;;; Copyright © 2017 ng0 <contact.ng0@cryptolab.net>
+;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
+;;; Copyright © 2017 Theodoros Foradis <theodoros.for@openmailbox.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
   #:use-module ((guix licenses) #:prefix license:)
   #:use-module (guix packages)
   #:use-module (guix download)
+  #:use-module (guix git-download)
   #:use-module (guix utils)
   #:use-module (guix build utils)
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
   #:use-module (guix build-system r)
   #:use-module (gnu packages algebra)
+  #:use-module (gnu packages autotools)
   #:use-module (gnu packages bison)
   #:use-module (gnu packages boost)
   #:use-module (gnu packages check)
   #:use-module (gnu packages less)
   #:use-module (gnu packages lisp)
   #:use-module (gnu packages logging)
+  #:use-module (gnu packages lua)
   #:use-module (gnu packages gnome)
   #:use-module (gnu packages guile)
   #:use-module (gnu packages xorg)
   #:use-module (gnu packages gl)
+  #:use-module (gnu packages imagemagick)
   #:use-module (gnu packages m4)
   #:use-module (gnu packages mpi)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages netpbm)
+  #:use-module (gnu packages ocaml)
   #:use-module (gnu packages pcre)
   #:use-module (gnu packages popt)
   #:use-module (gnu packages perl)
@@ -80,6 +90,7 @@
   #:use-module (gnu packages python)
   #:use-module (gnu packages readline)
   #:use-module (gnu packages tbb)
+  #:use-module (gnu packages scheme)
   #:use-module (gnu packages shells)
   #:use-module (gnu packages tcl)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages tls)
   #:use-module (gnu packages wxwidgets)
   #:use-module (gnu packages xml)
-  #:use-module (gnu packages zip)
   #:use-module (srfi srfi-1))
 
+(define-public aris
+  (package
+    (name "aris")
+    (version "2.2")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "mirror://gnu/" name "/" name "-" version ".tar.gz"))
+              (sha256 (base32
+                       "1q1887ryqdr9sn0522hc7p16kqwlxxyz5dkmma8ar2nxplhgll7q"))))
+    (build-system gnu-build-system)
+    (inputs `(("gtk+" ,gtk+)
+              ("libxml2" ,libxml2)))
+    (native-inputs `(("pkg-config" ,pkg-config)))
+    (synopsis "Natural deduction first-order logic interface")
+    (description "Aris is a program for performing logical proofs.  It supports
+propositional and predicate logic, as well as Boolean algebra and
+arithmetical logic.  In addition to its predefined inference and equivalence
+rules, Aris also supports references to older proofs.  Its use of standard
+logical symbols and its natural deduction interface make it easy to use for
+beginners.")
+    (license license:gpl3+)
+    (home-page "https://www.gnu.org/software/aris/")))
+
 (define-public c-graph
   (package
    (name "c-graph")
@@ -111,19 +144,19 @@ theory in visualizing the convolution process.  Rather than forcing the
 student to write code, the program offers an intuitive interface with
 interactive dialogs to guide them.")
    (license license:gpl3+)
-   (home-page "http://www.gnu.org/software/c-graph/")))
+   (home-page "https://www.gnu.org/software/c-graph/")))
 
 (define-public coda
   (package
     (name "coda")
-    (version "2.17.3")
+    (version "2.18")
     (source
      (origin
        (method url-fetch)
        (uri (string-append "https://github.com/stcorp/coda/releases/download/"
                            version "/coda-" version ".tar.gz"))
        (sha256
-        (base32 "04b9l3wzcix0mnfq77mwnil6cbr8h2mki8myvy0lzn236qcwaq1h"))
+        (base32 "11asla1ap8vd73farqjlpb179sfiy0biydcwxjfcakrp9sf8v9bs"))
        (patches (search-patches "coda-use-system-libs.patch"))
        (modules '((guix build utils)))
        (snippet
@@ -157,13 +190,13 @@ programming languages.")
 (define-public units
   (package
    (name "units")
-   (version "2.13")
+   (version "2.14")
    (source (origin
             (method url-fetch)
             (uri (string-append "mirror://gnu/units/units-" version
                                 ".tar.gz"))
             (sha256 (base32
-                     "1awhjw9zjlfb8s5g3yyx63f7ddfcr1sanlbxpqifmrgq24ql198b"))))
+                     "1s421bxm36akjsy3qzg6da1d1g20gh094ac2slqxipgkh8yqjcwx"))))
    (build-system gnu-build-system)
    (synopsis "Conversion between thousands of scales")
    (description
@@ -173,7 +206,7 @@ prefixes (micro-, kilo-, etc.).  It can also handle nonlinear
 conversions such as Fahrenheit to Celsius.  Its interpreter is powerful
 enough to be used effectively as a scientific calculator.")
    (license license:gpl3+)
-   (home-page "http://www.gnu.org/software/units/")))
+   (home-page "https://www.gnu.org/software/units/")))
 
 (define-public double-conversion
   (package
@@ -222,24 +255,29 @@ searched using a simple command-line tool, choosing from three databases:
 universal constants, atomic numbers, and constants related to
 semiconductors.")
     (license license:gpl3+)
-    (home-page "http://www.gnu.org/software/dionysus/")))
+    (home-page "https://www.gnu.org/software/dionysus/")))
 
 (define-public gsl
   (package
     (name "gsl")
-    (version "2.2.1")
+    (version "2.4")
     (source (origin
               (method url-fetch)
               (uri (string-append "mirror://gnu/gsl/gsl-"
                                   version ".tar.gz"))
               (sha256
                (base32
-                "095hp01d8lkqdvv0p1k25kvbisgfdmvx1rzpyc2i8kl2n33kvlhk"))
+                "16yfs5n444s03np1naj6yp1fsysd42kdscxzkg0k2yvfjixx0ijd"))
               (patches (search-patches "gsl-test-i686.patch"))))
     (build-system gnu-build-system)
     (arguments
-     `(#:parallel-tests? #f))
-    (home-page "http://www.gnu.org/software/gsl/")
+     `(;; Currently there are numerous tests that fail on "exotic"
+       ;; architectures such as aarch64 and ppc64le.
+       ,@(if (string-prefix? "aarch64-linux"
+                             (or (%current-target-system) (%current-system)))
+           '(#:tests? #f)
+           '())))
+    (home-page "https://www.gnu.org/software/gsl/")
     (synopsis "Numerical library for C and C++")
     (description
      "The GNU Scientific Library is a library for numerical analysis in C
@@ -249,10 +287,37 @@ differential equations, linear algebra, Fast Fourier Transforms and random
 numbers.")
     (license license:gpl3+)))
 
+(define-public ocaml-gsl
+  (package
+    (name "ocaml-gsl")
+    (version "1.19.3")
+    (source
+     (origin
+       (method url-fetch)
+       (uri
+        (string-append
+         "https://github.com/mmottl/gsl-ocaml/releases/download/v"
+         version"/gsl-ocaml-" version ".tar.gz"))
+       (sha256
+        (base32
+         "0nzp43hp8pbjqkrxnwp5lgjrabxayf61h18fjaydi0s5faq6f3xh"))))
+    (build-system ocaml-build-system)
+    (inputs
+     `(("gsl" ,gsl)))
+    (home-page "https://mmottl.github.io/gsl-ocaml")
+    (synopsis "Bindings to the GNU Scientific Library")
+    (description
+     "GSL-OCaml is an interface to the @dfn{GNU scientific library} (GSL) for
+the OCaml language.")
+    (license license:gpl3+)))
+
+(define-public ocaml4.01-gsl
+  (package-with-ocaml4.01 ocaml-gsl))
+
 (define-public glpk
   (package
     (name "glpk")
-    (version "4.60")
+    (version "4.63")
     (source
      (origin
       (method url-fetch)
@@ -260,13 +325,13 @@ numbers.")
                           version ".tar.gz"))
       (sha256
        (base32
-        "15z2ymzqhxwss6wgdj5f7vkyqlqdsjgrvm0x871kmlx0n0664mhk"))))
+        "1xp7nclmp8inp20968bvvfcwmz3mz03sbm0v3yjz8aqwlpqjfkci"))))
     (build-system gnu-build-system)
     (inputs
      `(("gmp" ,gmp)))
     (arguments
      `(#:configure-flags '("--with-gmp")))
-    (home-page "http://www.gnu.org/software/glpk/")
+    (home-page "https://www.gnu.org/software/glpk/")
     (synopsis "GNU Linear Programming Kit, supporting the MathProg language")
     (description
      "GLPK is a C library for solving large-scale linear programming (LP),
@@ -310,7 +375,7 @@ integer programming problems and computes Markov bases for statistics.")
     (source
      (origin
       (method url-fetch)
-      (uri (string-append "ftp://ftp.ifor.math.ethz.ch/pub/fukuda/cdd/cddlib-"
+      (uri (string-append "ftp://ftp.math.ethz.ch/users/fukudak/cdd/cddlib-"
                           (string-delete #\. version) ".tar.gz"))
       (sha256
        (base32
@@ -365,7 +430,7 @@ large scale eigenvalue problems.")
 (define-public lapack
   (package
     (name "lapack")
-    (version "3.5.0")
+    (version "3.7.1")
     (source
      (origin
       (method url-fetch)
@@ -373,14 +438,24 @@ large scale eigenvalue problems.")
                           version ".tgz"))
       (sha256
        (base32
-        "0lk3f97i9imqascnlf6wr5mjpyxqcdj73pgj97dj2mgvyg9z1n4s"))))
+        "1j51r7n5w4k7r3lrvy7710xrpkg40wf4rqnmngfz6ck9ypckzign"))))
     (build-system cmake-build-system)
     (home-page "http://www.netlib.org/lapack/")
     (inputs `(("fortran" ,gfortran)
               ("python" ,python-2)))
     (arguments
-     `(#:configure-flags '("-DBUILD_SHARED_LIBS:BOOL=YES"
-                           "-DLAPACKE=ON")
+     `(#: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"
+
+                          ;; Build the 'LAPACKE_clatms' functions.
+                          "-DLAPACKE_WITH_TMG=ON")
        #:phases (alist-cons-before
                  'check 'patch-python
                  (lambda* (#:key inputs #:allow-other-keys)
@@ -425,40 +500,37 @@ singular value problems.")
                                 "See LICENSE in the distribution."))))
 
 (define-public gnuplot
-  ;; Gnuplot version 5.0.4 was updated in-place, resulting in a hash mismatch.
-  ;; This can be removed at the next version update.
-  (let ((upstream-version "5.0.4")
-        (guix-revision "1"))
-    (package
-      (name "gnuplot")
-      (version (string-append upstream-version "-" guix-revision))
-      (source
-       (origin
-        (method url-fetch)
-        (uri (string-append "mirror://sourceforge/gnuplot/gnuplot/"
-                            upstream-version "/gnuplot-"
-                            upstream-version ".tar.gz"))
-        (sha256
-         (base32
-          "07n3w12dkcxjnhsvsliaqnkhajhi818v6q8mkpmpbplbf92vh70m"))))
-      (build-system gnu-build-system)
-      (inputs `(("readline" ,readline)
-                ("cairo" ,cairo)
-                ("pango" ,pango)
-                ("gd" ,gd)))
-      (native-inputs `(("pkg-config" ,pkg-config)
-                       ("texlive" ,texlive-minimal)))
-      (home-page "http://www.gnuplot.info")
-      (synopsis "Command-line driven graphing utility")
-      (description "Gnuplot is a portable command-line driven graphing
+  (package
+    (name "gnuplot")
+    (version "5.0.6")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "mirror://sourceforge/gnuplot/gnuplot/"
+                                  version "/gnuplot-"
+                                  version ".tar.gz"))
+       (sha256
+        (base32
+         "0q5lr6nala3ln6f3yp6g17ziymb9r9gx9zylnw1y3hjmwl9lggjv"))))
+    (build-system gnu-build-system)
+    (inputs `(("readline" ,readline)
+              ("cairo" ,cairo)
+              ("pango" ,pango)
+              ("gd" ,gd)
+              ("lua" ,lua)))
+    (native-inputs
+     `(("pkg-config" ,pkg-config)
+       ("texlive" ,texlive-tiny)))
+    (home-page "http://www.gnuplot.info")
+    (synopsis "Command-line driven graphing utility")
+    (description "Gnuplot is a portable command-line driven graphing
 utility.  It was originally created to allow scientists and students to
 visualize mathematical functions and data interactively, but has grown to
 support many non-interactive uses such as web scripting.  It is also used as a
 plotting engine by third-party applications like Octave.")
-      ;;  X11 Style with the additional restriction that derived works may only be
-      ;;  distributed as patches to the original.
-      (license (license:fsf-free
-                "http://gnuplot.cvs.sourceforge.net/gnuplot/gnuplot/Copyright")))))
+    ;;  X11 Style with the additional restriction that derived works may only be
+    ;;  distributed as patches to the original.
+    (license (license:fsf-free
+              "http://gnuplot.cvs.sourceforge.net/gnuplot/gnuplot/Copyright"))))
 
 (define-public gctp
   (package
@@ -489,18 +561,17 @@ computations.")
 (define-public hdf4
   (package
     (name "hdf4")
-    (version "4.2.11")
+    (version "4.2.13")
     (source
      (origin
        (method url-fetch)
        (uri (string-append "https://support.hdfgroup.org/ftp/HDF/releases/HDF"
                            version "/src/hdf-" version ".tar.bz2"))
        (sha256
-        (base32 "16yr50j845zlfx20skmw3y75ww77akk9gg0affjqkg66ih5r03mv"))
+        (base32 "1wz0586zh91pqb95wvr0pbh71a8rz358fdj6n2ksp85x2cis9lsm"))
        (patches (search-patches "hdf4-architectures.patch"
                                 "hdf4-reproducibility.patch"
                                 "hdf4-shared-fortran.patch"))))
-
     (build-system gnu-build-system)
     (native-inputs
      `(("gfortran" ,gfortran)
@@ -549,12 +620,13 @@ incompatible with HDF5.")
 (define-public hdf5
   (package
     (name "hdf5")
-    (version "1.8.18")
+    (version "1.8.19")
     (source
      (origin
       (method url-fetch)
-      (uri (list (string-append "http://www.hdfgroup.org/ftp/HDF5/releases/"
-                                "hdf5-" version "/src/hdf5-"
+      (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"
@@ -562,7 +634,7 @@ incompatible with HDF5.")
                                        (take (string-split version #\.) 2))
                                 "/src/hdf5-" version ".tar.bz2")))
       (sha256
-       (base32 "13542vrnl1p35n8vbq0wzk40vddmm33q5nh04j98c7r1yjnxxih1"))
+       (base32 "0f3jfbqpaaq21ighi40qzs52nb52kc2d2yjk541rjmsx20b3ih2r"))
       (patches (list (search-patch "hdf5-config-date.patch")))))
     (build-system gnu-build-system)
     (inputs
@@ -711,6 +783,38 @@ Swath).")
 HDF5 file is encoded according to the HDF File Format Specification.")
     (license (license:x11-style "file://COPYING"))))
 
+(define-public itpp
+  (package
+    (name "itpp")
+    (version "4.3.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "mirror://sourceforge/itpp/itpp/"
+                                  version "/itpp-"
+                                  version ".tar.gz"))
+       (sha256
+        (base32
+         "14ddy2xnb6sgp4hiax9v5sv4pr4l4dd4ps76nfha3nrpr1ikhcqm"))))
+    (build-system cmake-build-system)
+    (arguments `(#:tests? #f)) ; Tests require googletest *sources*
+    (inputs `(("lapack" ,lapack)
+              ("fftw" ,fftw)))
+    ;; FIXME: Even though the fonts are available dvips complains:
+    ;; "Font cmmi10 not found; characters will be left blank."
+    (native-inputs
+     `(("texlive" ,texlive-tiny)
+       ("ghostscript" ,ghostscript)
+       ("doxygen" ,doxygen)))
+    (home-page "http://itpp.sourceforge.net")
+    (synopsis "C++ library of maths, signal processing and communication classes")
+    (description "IT++ is a C++ library of mathematical, signal processing and
+communication classes and functions.  Its main use is in simulation of
+communication systems and for performing research in the area of
+communications.  The kernel of the library consists of generic vector and
+matrix classes, and a set of accompanying routines.  Such a kernel makes IT++
+similar to MATLAB, GNU Octave or SciPy.")
+    (license license:gpl3+)))
+
 (define-public netcdf
   (package
     (name "netcdf")
@@ -731,10 +835,12 @@ HDF5 file is encoded according to the HDF File Format Specification.")
        ("doxygen" ,doxygen)
        ("graphviz" ,graphviz)))
     (inputs
-     `(("hdf5" ,hdf5)
-       ("zlib" ,zlib)))
+     `(("hdf4" ,hdf4-alt)
+       ("hdf5" ,hdf5)
+       ("zlib" ,zlib)
+       ("libjpeg" ,libjpeg)))
     (arguments
-     `(#:configure-flags '("--enable-doxygen" "--enable-dot")
+     `(#:configure-flags '("--enable-doxygen" "--enable-dot" "--enable-hdf4")
        #:parallel-tests? #f))           ;various race conditions
     (home-page "http://www.unidata.ucar.edu/software/netcdf/")
     (synopsis "Library for scientific data")
@@ -762,6 +868,30 @@ sharing of scientific data.")
                 "--disable-shared" "--with-pic"
                 ,flags))))))
 
+(define-public netcdf-fortran
+  (package
+    (name "netcdf-fortran")
+    (version "4.4.4")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "ftp://ftp.unidata.ucar.edu/pub/netcdf/netcdf-fortran-"
+                    version ".tar.gz"))
+              (sha256
+               (base32
+                "0xaxdcg1p83zmypwml3swsnr3ccn38inwldyr1l3wa4dbwbrblxj"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:parallel-tests? #f))
+    (inputs
+     `(("netcdf" ,netcdf)))
+    (native-inputs
+     `(("gfortran" ,gfortran)))
+    (synopsis "Fortran interface for the netCDF library")
+    (description (package-description netcdf))
+    (home-page (package-home-page netcdf))
+    (license (package-license netcdf))))
+
 (define-public nlopt
   (package
     (name "nlopt")
@@ -900,7 +1030,7 @@ can solve two kinds of problems:
 (define-public octave
   (package
     (name "octave")
-    (version "4.2.0")
+    (version "4.2.1")
     (source
      (origin
       (method url-fetch)
@@ -908,11 +1038,12 @@ can solve two kinds of problems:
                           version ".tar.lz"))
       (sha256
        (base32
-        "19vvliwxgip0af812vny5xy5r8kacyj7v62203mh4z2n3p14b78i"))))
+        "09zhhch79jw3ynw39vizx0i2cbd2bjz3sp38pjdzraqrbivpwp92"))))
     (build-system gnu-build-system)
     (inputs
      `(("lapack" ,lapack)
        ("readline" ,readline)
+       ("gl2ps" ,gl2ps)
        ("glpk" ,glpk)
        ("fftw" ,fftw)
        ("fftwf" ,fftwf)
@@ -925,7 +1056,9 @@ can solve two kinds of problems:
        ("libxft" ,libxft)
        ("mesa" ,mesa)
        ("glu" ,glu)
-       ("zlib" ,zlib)))
+       ("zlib" ,zlib)
+       ("curl" ,curl)
+       ("graphicsmagick" ,graphicsmagick)))
     (native-inputs
      `(("lzip" ,lzip)
        ("gfortran" ,gfortran)
@@ -956,17 +1089,72 @@ Work may be performed both at the interactive command-line as well as via
 script files.")
     (license license:gpl3+)))
 
+(define-public opencascade-oce
+  (package
+    (name "opencascade-oce")
+    (version "0.17.2")
+    (source
+      (origin
+        (method url-fetch)
+        (uri (string-append
+               "https://github.com/tpaviot/oce/archive/OCE-"
+               version
+               ".tar.gz"))
+        (sha256
+          (base32
+            "0vpmnb0k5y2f7lpmwx9pg9yfq24zjvnsak5alzacncfm1hv9b6cd"))))
+    (build-system cmake-build-system)
+    (arguments
+     '(#:configure-flags
+        (list "-DOCE_TESTING:BOOL=ON"
+              "-DOCE_USE_TCL_TEST_FRAMEWORK:BOOL=ON"
+              "-DOCE_DRAW:BOOL=ON"
+              (string-append "-DOCE_INSTALL_PREFIX:PATH="
+                        (assoc-ref %outputs "out"))
+              "-UCMAKE_INSTALL_RPATH")))
+    (inputs
+      `(("freetype" ,freetype)
+        ("glu" ,glu)
+        ("libxmu" ,libxmu)
+        ("mesa" ,mesa)
+        ("tcl" ,tcl)
+        ("tk" ,tk)))
+    (native-inputs
+      `(("python" ,python-wrapper)))
+    (home-page "https://github.com/tpaviot/oce")
+    (synopsis "Libraries for 3D modeling and numerical simulation")
+    (description
+     "Open CASCADE is a set of libraries for the development of applications
+dealing with 3D CAD data or requiring industrial 3D capabilities.  It includes
+C++ class libraries providing services for 3D surface and solid modeling, CAD
+data exchange, and visualization.  It is used for development of specialized
+software dealing with 3D models in design (CAD), manufacturing (CAM),
+numerical simulation (CAE), measurement equipment (CMM), and quality
+control (CAQ) domains.
+
+This is the ``Community Edition'' (OCE) of Open CASCADE, which gathers
+patches, improvements, and experiments contributed by users over the official
+Open CASCADE library.")
+    (license (list license:lgpl2.1; OCE libraries, with an exception for the
+                                  ; use of header files; see
+                                  ; OCCT_LGPL_EXCEPTION.txt
+                   license:public-domain; files
+                                  ; src/Standard/Standard_StdAllocator.hxx and
+                                  ; src/NCollection/NCollection_StdAllocator.hxx
+                   license:expat; file src/OpenGl/OpenGl_glext.h
+                   license:bsd-3)))); test framework gtest
+
 (define-public gmsh
   (package
     (name "gmsh")
-    (version "2.14.1")
+    (version "2.16.0")
     (source
      (origin
       (method url-fetch)
       (uri (string-append "http://gmsh.info/src/gmsh-"
                           version "-source.tgz"))
       (sha256
-       (base32 "1vsxp47j6srmy8kqb3p1z9pmlm42whhhz7r0vzpa2a86gga4zx17"))
+       (base32 "1slf0bfkwrcgn6296wb4qhbk4ahz6i4wfb10hnim08x05vrylag8"))
       (modules '((guix build utils)))
       (snippet
        ;; Remove non-free METIS code
@@ -980,6 +1168,7 @@ script files.")
        ("lapack" ,lapack)
        ("mesa" ,mesa)
        ("glu" ,glu)
+       ("opencascade-oce" ,opencascade-oce)
        ("libx11" ,libx11)
        ("libxext" ,libxext)))
     (inputs
@@ -988,15 +1177,7 @@ script files.")
     (arguments
      `(#:configure-flags `("-DENABLE_METIS:BOOL=OFF"
                            "-DENABLE_BUILD_SHARED:BOOL=ON"
-                           "-DENABLE_BUILD_DYNAMIC:BOOL=ON")
-       #:phases (modify-phases %standard-phases
-                  (replace
-                   'check
-                   (lambda _
-                     (zero? (system* "make" "test"
-                                     ;; Disable this test.  See
-                                     ;; https://geuz.org/trac/gmsh/ticket/271
-                                     "ARGS=-E component8_in_a_box")))))))
+                           "-DENABLE_BUILD_DYNAMIC:BOOL=ON")))
     (home-page "http://www.geuz.org/gmsh/")
     (synopsis "3D finite element grid generator")
     (description "Gmsh is a 3D finite element grid generator with a built-in
@@ -1008,10 +1189,34 @@ 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 maxflow
+  (package
+    (name "maxflow")
+    (version "3.04")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/gerddie/maxflow.git")
+                    (commit "42401fa54823d16b9da47716f04e5d9ef1605875")))
+              (file-name (string-append name "-" version "-checkout"))
+              (sha256
+               (base32
+                "0rll38whw55h0vcjrrwdnh9ascvxby0ph7n1l0d12z17cg215kkb"))))
+    (build-system cmake-build-system)
+    (home-page "http://pub.ist.ac.at/~vnk/software.html")
+    (synopsis "Library implementing Maxflow algorithm")
+    (description "An implementation of the maxflow algorithm described in
+@cite{An Experimental Comparison of Min-Cut/Max-Flow Algorithms for
+Energy Minimization in Computer Vision.\n
+Yuri Boykov and Vladimir Kolmogorov.\n
+In IEEE Transactions on Pattern Analysis and Machine Intelligence,\n
+September 2004}")
+    (license license:gpl3+)))
+
 (define-public petsc
   (package
     (name "petsc")
-    (version "3.7.2")
+    (version "3.7.6")
     (source
      (origin
       (method url-fetch)
@@ -1019,7 +1224,7 @@ ASCII text files using Gmsh's own scripting language.")
       (uri (string-append "http://ftp.mcs.anl.gov/pub/petsc/release-snapshots/"
                           "petsc-lite-" version ".tar.gz"))
       (sha256
-       (base32 "0jfrq6rd4zagw1iimz05m2w91k0jvz3qbik1lk8pqcxw3rvdqk5d"))))
+       (base32 "1y3f5jjq0v5b62i3sabp4kp5mgfyp3vnk0dxhwkrhpypax77nzxh"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("python" ,python-2)
@@ -1042,6 +1247,10 @@ ASCII text files using Gmsh's own scripting language.")
                          (assoc-ref %build-inputs "superlu") "/include")
          ,(string-append "--with-superlu-lib="
                          (assoc-ref %build-inputs "superlu") "/lib/libsuperlu.a"))
+       #:make-flags
+       ;; Honor (parallel-job-count) for build.  Do not use --with-make-np,
+       ;; whose value is dumped to $out/lib/petsc/conf/petscvariables.
+       (list (format #f "MAKE_NP=~a" (parallel-job-count)))
        #:phases
        (modify-phases %standard-phases
         (replace 'configure
@@ -1056,13 +1265,17 @@ ASCII text files using Gmsh's own scripting language.")
               (format #t "configure flags: ~s~%" flags)
               (zero? (apply system* "./configure" flags)))))
         (add-after 'configure 'clean-local-references
-          (lambda* (#:key inputs outputs #:allow-other-keys)
+          (lambda* (#:key outputs #:allow-other-keys)
             (let ((out (assoc-ref outputs "out")))
               (substitute* (find-files "." "^petsc(conf|machineinfo).h$")
                 ;; Prevent build directory from leaking into compiled code
                 (((getcwd)) out)
                 ;; Scrub timestamp for reproducibility
                 ((".*Libraries compiled on.*") ""))
+              (substitute* (find-files "." "petscvariables")
+                ;; Do not expose build machine characteristics, set to defaults.
+                (("MAKE_NP = [:digit:]+") "MAKE_NP = 2")
+                (("NPMAX = [:digit:]+") "NPMAX = 2"))
               #t)))
         (add-after 'install 'clean-install
           ;; Try to keep installed files from leaking build directory names.
@@ -1137,16 +1350,15 @@ scientific applications modeled by partial differential equations.")
 (define-public slepc
   (package
     (name "slepc")
-    (version "3.7.1")
+    (version "3.7.4")
     (source
      (origin
        (method url-fetch)
-       (uri (string-append "http://slepc.upv.es/download/download.php?"
-                           "filename=slepc-" version ".tar.gz"))
-       (file-name (string-append name "-" version ".tar.gz"))
+       (uri (string-append "http://slepc.upv.es/download/distrib/slepc-"
+                           version ".tar.gz"))
        (sha256
         (base32
-         "1hijlmrvxvfqslnx8yydzw5xqbsn1yy02g32w0hln1z3cgr1c0k7"))))
+         "12pbl8yd6r8k9xjlr1qw25rs0k1acgic7hw1s6l6bhiv9s285drg"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("python" ,python-2)))
@@ -1160,6 +1372,8 @@ scientific applications modeled by partial differential equations.")
        #:configure-flags
        `(,(string-append "--with-arpack-dir="
                          (assoc-ref %build-inputs "arpack") "/lib"))
+       #:make-flags                     ;honor (parallel-job-count)
+       `(,(format #f "MAKE_NP=~a" (parallel-job-count)))
        #:phases
        (modify-phases %standard-phases
          (replace 'configure
@@ -1421,12 +1635,12 @@ programming problems.")
 (define-public r-pracma
   (package
     (name "r-pracma")
-    (version "1.9.5")
+    (version "2.0.7")
     (source (origin
       (method url-fetch)
       (uri (cran-uri "pracma" version))
       (sha256
-        (base32 "19nr2jlkbcdgvw3gx5hry12av565lmvqd5q4h7zlch3q13avwwl2"))))
+        (base32 "0hxa0rbbp54j0c05qj7vfwhqfdmiz5ax8vhqxd09g33x7c0hqbc5"))))
     (build-system r-build-system)
     (propagated-inputs
      `(("r-quadprog" ,r-quadprog)))
@@ -1645,7 +1859,7 @@ implemented in ANSI C, and MPI for communications.")
     (build-system gnu-build-system)
     (inputs
      `(("zlib" ,zlib)
-       ("flex" ,flex)
+       ("flex" ,flex-2.6.1) ; A bug in flex prevents building with flex-2.6.3.
        ("bison" ,bison)))
     (arguments
      `(#:phases
@@ -1683,6 +1897,7 @@ YACC = bison -pscotchyy -y -b y
                         '("COMMON_FILE_COMPRESS_GZ"
                           "COMMON_PTHREAD"
                           "COMMON_RANDOM_FIXED_SEED"
+                          "INTSIZE64"             ;use 'long' instead of 'int'
                           ;; Prevents symbolc clashes with libesmumps
                           "SCOTCH_RENAME"
                           ;; XXX: Causes invalid frees in superlu-dist tests
@@ -1844,7 +2059,7 @@ processor cores.")
        ("popt" ,popt)))
     (native-inputs
      `(("pkg-config" ,pkg-config)))
-    (home-page "http://www.gnu.org/software/gsegrafix/")
+    (home-page "https://www.gnu.org/software/gsegrafix/")
     (synopsis "GNOME application to create scientific and engineering plots")
     (description  "GSEGrafix is an application which produces high-quality graphical
 plots for science and engineering.  Plots are specified via simple ASCII
@@ -1857,7 +2072,7 @@ to BMP, JPEG or PNG image formats.")
 (define-public maxima
   (package
     (name "maxima")
-    (version "5.38.1")
+    (version "5.40.0")
     (source
      (origin
        (method url-fetch)
@@ -1865,7 +2080,7 @@ to BMP, JPEG or PNG image formats.")
                            version "-source/" name "-" version ".tar.gz"))
        (sha256
         (base32
-         "1p6646rvq43hk09msyp0dk50cqpkh07mf4x0bc2fqisqmcv6b1hf"))
+         "15pp35ayglv723bjbqc60gcdv2bm54s6pywsm4i4cwbjsf64dzkl"))
        (patches (search-patches "maxima-defsystem-mkdir.patch"))))
     (build-system gnu-build-system)
     (inputs
@@ -1891,36 +2106,43 @@ to BMP, JPEG or PNG image formats.")
        ;; '/tmp/nix-build-maxima-*', which won't exist at run time.
        ;; Work around that.
        #:make-flags (list "TMPDIR=/tmp")
-       #:phases (alist-cons-before
-                 'check 'pre-check
-                 (lambda _
-                   (chmod "src/maxima" #o555))
-                 ;; Make sure the doc and emacs files are found in the
-                 ;; standard location.  Also configure maxima to find gnuplot
-                 ;; without having it on the PATH.
-                 (alist-cons-after
-                  'install 'post-install
-                  (lambda* (#:key outputs inputs #:allow-other-keys)
-                    (let* ((gnuplot (assoc-ref inputs "gnuplot"))
-                          (out (assoc-ref outputs "out"))
-                          (datadir (string-append out "/share/maxima/" ,version)))
-                      (with-directory-excursion out
-                        (mkdir-p "share/emacs")
-                        (mkdir-p "share/doc")
-                        (symlink
-                         (string-append datadir "/emacs/")
-                         (string-append out "/share/emacs/site-lisp"))
-                        (symlink
-                         (string-append datadir "/doc/")
-                         (string-append out "/share/doc/maxima"))
-                        (with-atomic-file-replacement
-                         (string-append datadir "/share/maxima-init.lisp")
-                         (lambda (in out)
-                           (format out "~a ~s~a~%"
-                                   "(setf $gnuplot_command "
-                                   (string-append gnuplot "/bin/gnuplot") ")")
-                           (dump-port in out))))))
-                  %standard-phases))))
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'check 'pre-check
+           (lambda _
+             (chmod "src/maxima" #o555)
+             #t))
+         ;; Make sure the doc and emacs files are found in the
+         ;; standard location.  Also configure maxima to find gnuplot
+         ;; without having it on the PATH.
+         (add-after 'install 'post-install
+           (lambda* (#:key outputs inputs #:allow-other-keys)
+             (let* ((gnuplot (assoc-ref inputs "gnuplot"))
+                    (out (assoc-ref outputs "out"))
+                    (datadir (string-append out "/share/maxima/" ,version))
+                    (binutils (string-append (assoc-ref inputs "binutils")
+                                             "/bin")))
+               (with-directory-excursion out
+                 (mkdir-p "share/emacs")
+                 (mkdir-p "share/doc")
+                 (symlink
+                  (string-append datadir "/emacs/")
+                  (string-append out "/share/emacs/site-lisp"))
+                 (symlink
+                  (string-append datadir "/doc/")
+                  (string-append out "/share/doc/maxima"))
+                 (with-atomic-file-replacement
+                  (string-append datadir "/share/maxima-init.lisp")
+                  (lambda (in out)
+                    (format out "~a ~s~a~%"
+                            "(setf $gnuplot_command "
+                            (string-append gnuplot "/bin/gnuplot") ")")
+                    (dump-port in out))))
+               ;; Ensure that Maxima will have access to the GNU binutils
+               ;; components at runtime.
+               (wrap-program (string-append out "/bin/maxima")
+                 `("PATH" prefix (,binutils))))
+             #t)))))
     (home-page "http://maxima.sourceforge.net")
     (synopsis "Numeric and symbolic expression manipulation")
     (description "Maxima is a system for the manipulation of symbolic and
@@ -1937,16 +2159,21 @@ point numbers.")
 (define-public wxmaxima
   (package
     (name "wxmaxima")
-    (version "16.04.2")
+    (version "17.05.0")
     (source
      (origin
        (method url-fetch)
-       (uri (string-append "mirror://sourceforge/wxmaxima/wxMaxima/"
-                           version "/" name "-" version ".tar.gz"))
+       (uri (string-append "https://github.com/andrejv/" name "/archive"
+                           "/Version-" version ".tar.gz"))
+       (file-name (string-append name "-" version ".tar.gz"))
        (sha256
         (base32
-         "1fpqzk1921isiqrpgpf433ldq41924qs9sy99fl1zn5661b2l73n"))))
+         "1bsyd7r12xm2crpizb9iyyki3j0mbazzzwbsh871m06dv2wk97gq"))))
     (build-system gnu-build-system)
+    (native-inputs
+     `(("autoconf" ,autoconf)
+       ("automake" ,automake)
+       ("gettext" ,gettext-minimal)))
     (inputs
      `(("wxwidgets" ,wxwidgets)
        ("maxima" ,maxima)
@@ -1956,6 +2183,10 @@ point numbers.")
        ("shared-mime-info" ,shared-mime-info)))
     (arguments
      `(#:phases (modify-phases %standard-phases
+                  (add-before
+                   'configure 'autoconf
+                   (lambda _
+                     (zero? (system* "./bootstrap"))))
                   (add-after
                    'install 'wrap-program
                    (lambda* (#:key inputs outputs #:allow-other-keys)
@@ -1995,14 +2226,14 @@ full text searching.")
 (define-public armadillo
   (package
     (name "armadillo")
-    (version "7.500.0")
+    (version "7.800.2")
     (source (origin
               (method url-fetch)
               (uri (string-append "mirror://sourceforge/arma/armadillo-"
                                   version ".tar.xz"))
               (sha256
                (base32
-                "1x98d32cgxbzbbma2ak6c37wnbpq13xxyxyd6jjvflv748mzi9ks"))))
+                "1qqzy7dp891j9v7062mv1599hdwr97vqzrd3j2fl8c3gmc00dmzg"))))
     (build-system cmake-build-system)
     (arguments `(#:tests? #f)) ;no test target
     (inputs
@@ -2019,18 +2250,7 @@ environments.  It can be used for machine learning, pattern recognition,
 signal processing, bioinformatics, statistics, econometrics, etc.  The library
 provides efficient classes for vectors, matrices and cubes, as well as 150+
 associated functions (eg. contiguous and non-contiguous submatrix views).")
-    (license license:mpl2.0)))
-
-(define-public armadillo-for-rcpparmadillo
-  (package (inherit armadillo)
-    (version "7.500.0")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "mirror://sourceforge/arma/armadillo-"
-                                  version ".tar.xz"))
-              (sha256
-               (base32
-                "1x98d32cgxbzbbma2ak6c37wnbpq13xxyxyd6jjvflv748mzi9ks"))))))
+    (license license:asl2.0)))
 
 (define-public muparser
   ;; When switching download sites, muparser re-issued a 2.2.5 release with a
@@ -2087,7 +2307,8 @@ parts of it.")
         ,(let ((system (or (%current-target-system) (%current-system))))
            (or (string-prefix? "x86_64" system)
                (string-prefix? "i686" system)
-               (string-prefix? "mips" system)))
+               (string-prefix? "mips" system)
+               (string-prefix? "aarch64" system)))
        #:make-flags
        (list (string-append "PREFIX=" (assoc-ref %outputs "out"))
              "SHELL=bash"
@@ -2107,6 +2328,9 @@ parts of it.")
                   ;; for Loongson cores are used.
                   ((string-prefix? "mips" system)
                    '("TARGET=SICORTEX"))
+                  ;; On aarch64 force the generic 'armv8-a' target
+                  ((string-prefix? "aarch64" system)
+                   '("TARGET=ARMV8"))
                   (else '()))))
        ;; no configure script
        #:phases (alist-delete 'configure %standard-phases)))
@@ -2224,15 +2448,14 @@ Fresnel integrals, and similar related functions as well.")
              (string-append "INSTALL_INCLUDE="
                             (assoc-ref %outputs "out") "/include"))
        #:phases
-       (alist-cons-before
-        'install 'prepare-out
-        ;; README.txt states that the target directories must exist prior to
-        ;; running "make install".
-        (lambda _
-          (mkdir-p (string-append (assoc-ref %outputs "out") "/lib"))
-          (mkdir-p (string-append (assoc-ref %outputs "out") "/include")))
-        ;; no configure script
-        (alist-delete 'configure %standard-phases))))
+       (modify-phases %standard-phases
+         (delete 'configure)            ;no configure script
+         (add-before 'install 'prepare-out
+           ;; README.txt states that the target directories must exist prior to
+           ;; running "make install".
+           (lambda _
+             (mkdir-p (string-append (assoc-ref %outputs "out") "/lib"))
+             (mkdir-p (string-append (assoc-ref %outputs "out") "/include")))))))
     (inputs
      `(("tbb" ,tbb)
        ("lapack" ,lapack)))
@@ -2562,6 +2785,8 @@ in finite element programs.")
           (base32
             "022w8hph7bli5zbpnk3z1qh1c2sl5hm8fw2ccim651ynn0hr7fyz"))))
     (build-system cmake-build-system)
+    (outputs '("out"
+               "octave"))                  ;46 MiB .mex file that pulls Octave
     (native-inputs
      `(("unzip" ,unzip)))
     (inputs
@@ -2579,6 +2804,14 @@ in finite element programs.")
        ;; Save 12 MiB by not installing .a files.  Passing
        ;; '-DBUILD_STATIC_LIBS=OFF' has no effect.
        #:phases (modify-phases %standard-phases
+                  (add-before 'configure 'set-octave-directory
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      ;; Install the .mex file in the "octave" output.
+                      (let ((out (assoc-ref outputs "octave")))
+                        (substitute* "src/matlab/CMakeLists.txt"
+                          (("share/flann/octave")
+                           (string-append out "/share/flann/octave")))
+                        #t)))
                   (add-after 'install 'remove-static-libraries
                     (lambda* (#:key outputs #:allow-other-keys)
                       (let* ((out (assoc-ref outputs "out"))
@@ -2651,7 +2884,7 @@ patterns and allows you to zoom in and out of them infinitely in a fluid,
 continuous manner.  It also includes tutorials that help to explain how fractals
 are built.  It can generate many different fractal types such as the Mandelbrot
 set.")
-    (home-page "http://www.gnu.org/software/xaos/")
+    (home-page "https://www.gnu.org/software/xaos/")
     (license license:gpl2+)))
 
 (define-public hypre
@@ -2835,11 +3068,183 @@ compilers and compiler versions as well as portability between different vector
 instruction sets.  Thus, an application written with Vc can be compiled for:
 @enumerate
 @item AVX and AVX2
-@item SSE2 upto SSE4.2 or SSE4a
+@item SSE2 up to SSE4.2 or SSE4a
 @item Scalar
 @item MIC
 @item NEON (in development)
 @item NVIDIA GPUs / CUDA (in development)
 @end enumerate\n")
     (home-page "https://github.com/VcDevel/Vc")
+    ;; "No support_???.cpp file exists for this architecture."
+    (supported-systems '("x86_64-linux" "i686-linux"))
     (license license:bsd-3)))
+
+(define-public reducelcs
+  ;; This is the last commit which is available upstream, no
+  ;; release happened since 2010.
+  (let ((commit "474f88deb968061abe8cf11c959e02319b8ae5c0")
+        (revision "1"))
+    (package
+      (name "reducelcs")
+      (version (string-append "1.0-" revision "." (string-take commit 7)))
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference
+               (url "https://github.com/gdv/Reduce-Expand-for-LCS")
+               (commit commit)))
+         (file-name (string-append name "-" version "-checkout"))
+         (sha256
+          (base32
+           "1rllzcfwc042c336mhq262a8ha90x6afq30kvk60r7i4761j4yjm"))))
+      (build-system gnu-build-system)
+      (inputs
+       `(("openlibm" ,openlibm)))
+      (arguments
+       `(#:tests? #f ; no tests
+         #:phases
+         (modify-phases %standard-phases
+           (delete 'configure) ; No configure script exists.
+           (replace 'install ; No install phase exists.
+             (lambda* (#:key outputs #:allow-other-keys)
+               (let* ((out (assoc-ref outputs "out"))
+                      (bin (string-append out "/bin")))
+                 (install-file "Approximation" bin)
+                 (install-file "CollectResults" bin)
+                 (install-file "GenerateInstances" bin)
+                 #t))))))
+      (synopsis "Approximate Longest Commons Subsequence computation tool")
+      (description
+       "@code{reduceLCS} is an implementation of the Reduce-Expand
+algorithm for LCS.  It is a fast program to compute the approximate
+Longest Commons Subsequence of a set of strings.")
+      (home-page "https://github.com/gdv/Reduce-Expand-for-LCS")
+      (license license:gpl3+))))
+
+(define-public jacal
+  (package
+    (name "jacal")
+    (version "1c4")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "http://groups.csail.mit.edu/mac/ftpdir/scm/jacal-"
+                    version ".zip"))
+              (sha256 (base32
+                       "055zrn12a1dmy0dqkwrkq3fklbhg3yir6vn0lacp4mvbg8573a3q"))
+              (patches (search-patches "jacal-fix-texinfo.patch"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-before 'build 'pre-build
+                     ;; Don't use upstream's script - it really doesn't fit into
+                     ;; Guix's functional paradigm.
+                     (lambda* (#:key inputs outputs #:allow-other-keys)
+                       (substitute* "Makefile"
+                         (("^install: install-script") "install: "))))
+         (add-after 'install 'post-install
+                    ;; Instead, we provide our own simplified script.
+                    (lambda* (#:key inputs outputs #:allow-other-keys)
+                      (let ((wrapper (string-append (assoc-ref outputs "out")
+                                                    "/bin/jacal")))
+                        (format (open wrapper (logior O_WRONLY O_CREAT))
+                                (string-append "#!~a\nexec ~a/bin/scm -ip1 "
+                                "-e '(slib:load \"~a/lib/jacal/math\") "
+                                "(math)' \"$@\"\n")
+                                (which  "bash")
+                                (assoc-ref inputs "scm")
+                                (assoc-ref outputs "out"))
+                        (chmod wrapper #o555))))
+         (replace 'configure
+                  (lambda* (#:key inputs outputs #:allow-other-keys)
+                    (zero? (system* "./configure"
+                                    (string-append "--prefix="
+                                                   (assoc-ref outputs "out")))))))))
+    (inputs `(("scm" ,scm)))
+    (native-inputs `(("unzip" ,unzip)
+                     ("texinfo" ,texinfo)))
+    (synopsis "Symbolic mathematics system")
+    (description "GNU JACAL is an interactive symbolic mathematics program based on
+Scheme.  It manipulate and simplify a range of mathematical expressions such
+as equations, scalars, vectors, and matrices.")
+    (home-page "https://www.gnu.org/software/jacal/")
+    (license license:gpl3+)))
+
+(define-public z3
+  (package
+    (name "z3")
+    (version "4.5.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append
+                    "https://github.com/Z3Prover/z3/archive/z3-"
+                    version ".tar.gz"))
+              (sha256
+               (base32
+                "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
+    (build-system gnu-build-system)
+    (arguments
+     `(#:test-target "test"
+       #:phases
+       (modify-phases %standard-phases
+         (replace 'configure
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (zero?
+              (system* "python" "scripts/mk_make.py"
+                       (string-append "--prefix="
+                                      (assoc-ref outputs "out"))))))
+         (add-after 'configure 'change-dir
+           (lambda _
+             (chdir "build")
+             #t)))))
+    (native-inputs
+     `(("python" ,python-2)))
+    (synopsis "Theorem prover")
+    (description "Z3 is a theorem prover and @dfn{satisfiability modulo
+theories} (SMT) solver.  It provides a C/C++ API.")
+    (home-page "https://github.com/Z3Prover/z3")
+    (license license:expat)))
+
+(define-public cubicle
+  (package
+    (name "cubicle")
+    (version "1.1.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://cubicle.lri.fr/cubicle-"
+                                  version ".tar.gz"))
+              (sha256
+               (base32
+                "1sny9c4fm14k014pk62ibpwbrjjirkx8xmhs9jg7q1hk7y7x3q2h"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("which" ,(@@ (gnu packages base) which))))
+    (propagated-inputs
+     `(("z3" ,z3)))
+    (arguments
+     `(#:configure-flags (list "--with-z3")
+       #:tests? #f
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'configure-for-release
+           (lambda _
+             (substitute* "Makefile.in"
+               (("SVNREV=") "#SVNREV="))))
+         (add-before 'configure 'fix-/bin/sh
+           (lambda _
+             (substitute* "configure"
+               (("/bin/sh") (which "sh")))))
+         (add-before 'configure 'fix-smt-z3wrapper.ml
+           (lambda _
+             (substitute* "Makefile.in"
+               (("\\\\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.")
+    (license license:asl2.0)))