diff options
Diffstat (limited to 'gnu/packages/maths.scm')
| -rw-r--r-- | gnu/packages/maths.scm | 587 |
1 files changed, 486 insertions, 101 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 4640237968..1853c77a14 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -55,10 +55,11 @@ ;;; Copyright © 2022 Philip McGrath <[email protected]> ;;; Copyright © 2022 Marek Felšöci <[email protected]> ;;; Copyright © 2022 vicvbcun <[email protected]> -;;; Copyright © 2022 Liliana Marie Prikler <[email protected]> +;;; Copyright © 2022, 2023 Liliana Marie Prikler <[email protected]> ;;; Copyright © 2022 Maximilian Heisinger <[email protected]> ;;; Copyright © 2022 Akira Kyle <[email protected]> ;;; Copyright © 2022 Roman Scherer <[email protected]> +;;; Copyright © 2023 Jake Leporte <[email protected]> ;;; ;;; This file is part of GNU Guix. ;;; @@ -87,7 +88,9 @@ #:use-module (guix gexp) #:use-module (guix utils) #:use-module ((guix build utils) #:select (alist-replace)) + #:use-module (guix build-system ant) #:use-module (guix build-system cmake) + #:use-module (guix build-system copy) #:use-module (guix build-system glib-or-gtk) #:use-module (guix build-system gnu) #:use-module (guix build-system meson) @@ -103,6 +106,7 @@ #:use-module (gnu packages bash) #:use-module (gnu packages bison) #:use-module (gnu packages boost) + #:use-module (gnu packages calendar) #:use-module (gnu packages check) #:use-module (gnu packages cmake) #:use-module (gnu packages compression) @@ -123,7 +127,9 @@ #:use-module (gnu packages gd) #:use-module (gnu packages ghostscript) #:use-module (gnu packages glib) + #:use-module (gnu packages gperf) #:use-module (gnu packages graphviz) + #:use-module (gnu packages groff) #:use-module (gnu packages gtk) #:use-module (gnu packages icu4c) #:use-module (gnu packages image) @@ -151,6 +157,7 @@ #:use-module (gnu packages pcre) #:use-module (gnu packages popt) #:use-module (gnu packages perl) + #:use-module (gnu packages prolog) #:use-module (gnu packages pkg-config) #:use-module (gnu packages pulseaudio) #:use-module (gnu packages python) @@ -172,6 +179,7 @@ #:use-module (gnu packages tls) #:use-module (gnu packages version-control) #:use-module (gnu packages wxwidgets) + #:use-module (gnu packages xdisorg) #:use-module (gnu packages xml) #:use-module (srfi srfi-1) #:use-module (srfi srfi-26)) @@ -455,6 +463,101 @@ semiconductors.") (license license:gpl3+) (home-page "https://www.gnu.org/software/dionysus/"))) +(define-public dozenal + ;; There is no recent release, so use the latest commit. + (let ((revision "1") + (commit "328bc03ad544179f2cccda36763358c4216f188e")) + (package + (name "dozenal") + (version (git-version "12010904-3" revision commit)) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://codeberg.org/dgoodmaniii/dozenal") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0knwfwjqdv854l5ny7csdpvp7r0md6a2k43a1l2lkyw9k3cglpph")))) + (build-system gnu-build-system) + (arguments + (list + ;; Some test scripts are included, but no makefile-driven + ;; tests, and they are all quite manual to run and check. + #:tests? #f + ;; Running with `make -j' causes the build to fail. This is likely + ;; because this project uses the "recursive make" structure, where + ;; each subdirectory contains its own make file, which is called by + ;; the top-level makefile. + #:parallel-build? #f + #:make-flags + #~(list (string-append "prefix=" #$output)) + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'chdir + (lambda _ + (chdir "dozenal"))) + (add-after 'chdir 'patch-lua-references + (lambda _ + (let ((lua-name (strip-store-file-name + #$(this-package-input "lua")))) + (substitute* '("dozcal/Makefile" + "dozlua/Makefile") + (("lua52") + (string-take lua-name + (string-rindex lua-name #\.))))))) + (delete 'configure) + (add-before 'install 'make-bin-dir + (lambda _ + (mkdir-p (string-append #$output "/bin")))) + (add-after 'install 'install-html-docs + (lambda _ + (invoke "make" + (string-append "prefix=" #$output) + "installhtml"))) + (add-after 'install-html-docs 'split-outputs + (lambda* (#:key inputs outputs #:allow-other-keys) + (for-each + (lambda (prog) + (let ((orig (string-append #$output "/bin/" prog)) + (dst (string-append #$output:gui "/bin/" prog)) + (man-orig (string-append #$output + "/share/man/man1/" + prog ".1")) + (man-dst (string-append #$output:gui + "/share/man/man1/" + prog ".1"))) + (mkdir-p (dirname dst)) + (rename-file orig dst) + (mkdir-p (dirname man-dst)) + (rename-file man-orig man-dst))) + '("xdozdc" "gdozdc")) + (wrap-program (string-append #$output:gui "/bin/" "gdozdc") + `("PATH" = (,(string-append #$output "/bin"))) + `("PERL5LIB" = (,(getenv "PERL5LIB"))))))))) + (outputs '("out" "gui")) + (native-inputs (list groff pkg-config)) + (inputs (list bash-minimal ;for wrap-program + libhdate + lua + ncurses + perl + perl-tk + perl-par + xforms)) + (synopsis "Suite of dozenal programs") + (description + "The dozenal suite is a set of programs designed to assist with working +in the dozenal (also called \"duodecimal\" or \"base twelve\") system. It +includes number converters (dozenal-to-decimal and decimal-to-dozenal), an RPN +calculator, a graphical calculator, a metric system converter (works with +imperial, U.S. customary, SI metric, and the dozenal TGM), a pretty-printer +for dozenal numbers, a date-and-time program, and a dozenal calendar programs, +complete with events and to-dos.") + (home-page "https://codeberg.org/dgoodmaniii/dozenal") + (license license:gpl3+)))) + (define-public dsfmt (package (name "dsfmt") @@ -930,7 +1033,7 @@ large scale eigenvalue problems.") (base32 "1155qixp26c12yrxc76z9mlfw2h3xxymxxv5znpgzh5gaykpndgj")))) (build-system cmake-build-system) - (home-page "http://www.netlib.org/lapack/") + (home-page "https://www.netlib.org/lapack/") (inputs `(("fortran" ,gfortran) ("python" ,python-wrapper))) (arguments @@ -1033,7 +1136,7 @@ provide LAPACK for someone who does not have access to a Fortran compiler.") (substitute* "TESTING/CMakeLists.txt" (("^add_test\\(x[sd]hseqr.*" all) (string-append "# " all "\n")))))))) - (home-page "http://www.netlib.org/scalapack/") + (home-page "https://www.netlib.org/scalapack/") (synopsis "Library for scalable numerical linear algebra") (description "ScaLAPACK is a Fortran 90 library of high-performance linear algebra @@ -1655,7 +1758,7 @@ System (Grid, Point and Swath).") "HDF-EOS5 is a software library built on HDF5 to support the construction of data structures used in NASA's Earth Observing System (Grid, Point and Swath).") - (home-page "http://www.hdfeos.org/software/library.php#HDF-EOS5") + (home-page "https://www.hdfeos.org/software/library.php#HDF-EOS5") ;; Source files carry a permissive license header. (license (license:non-copyleft home-page)))) @@ -1840,7 +1943,7 @@ the resulting text.") `(("texlive" ,texlive-tiny) ("ghostscript" ,ghostscript) ("doxygen" ,doxygen))) - (home-page "http://itpp.sourceforge.net") + (home-page "https://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 @@ -2703,12 +2806,20 @@ satisfiability checking (SAT).") (package (inherit clingo) (name "python-clingo") + (version (package-version clingo)) ; for #$version in arguments (arguments (substitute-keyword-arguments (package-arguments clingo) ((#:configure-flags flags #~'()) #~(cons* "-DCLINGO_BUILD_WITH_PYTHON=pip" "-DCLINGO_USE_LIB=yes" #$flags)) + ((#:imported-modules _ '()) + `(,@%cmake-build-system-modules + (guix build python-build-system))) + ((#:modules _ '()) + '((guix build cmake-build-system) + ((guix build python-build-system) #:prefix python:) + (guix build utils))) ((#:phases phases #~%standard-phases) #~(modify-phases #$phases (add-after 'unpack 'fix-failing-tests @@ -2717,7 +2828,17 @@ satisfiability checking (SAT).") (("ctl\\.solve\\(on_statistics=on_statistics\\)" all) (string-append all - "; self.skipTest(\"You shall not fail.\")"))))))))) + "; self.skipTest(\"You shall not fail.\")"))))) + (add-after 'install 'install-distinfo + (lambda* (#:key inputs outputs #:allow-other-keys) + (with-directory-excursion (python:site-packages inputs outputs) + (let ((dir (string-append "clingo-" #$version ".dist-info"))) + (mkdir-p dir) + (call-with-output-file (string-append dir "/METADATA") + (lambda (port) + (format port "Metadata-Version: 1.1~%") + (format port "Name: clingo~%") + (format port "Version: ~a~%" #$version))))))))))) (inputs (list clingo python-wrapper)) (propagated-inputs (list python-cffi)) (native-inputs (modify-inputs (package-native-inputs clingo) @@ -2727,6 +2848,41 @@ satisfiability checking (SAT).") making it so that you can write @acronym{ASPs, Answer Set Programs} through Python code."))) +(define-public python-clorm + (package + (name "python-clorm") + (version "1.4.1") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/potassco/clorm") + (commit (string-append "v" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0jx99y71mrgdicn1da5dwz5nzgvvpabrikff783sg4shbv2cf0b5")))) + (build-system pyproject-build-system) + (arguments + (list #:phases + #~(modify-phases %standard-phases + (add-before 'check 'fix-breaking-tests + (lambda _ + ;; noclingo tests rely on this being set + (setenv "CLORM_NOCLINGO" "1") + (delete-file "tests/test_mypy_query.py") + (substitute* "tests/test_clingo.py" + (("self\\.assertTrue\\(os_called\\)" all) + (string-append "# " all)))))))) + (propagated-inputs (list python-clingo)) + (native-inputs (list python-typing-extensions)) + (home-page "https://potassco.org") + (synopsis "Object relational mapping to clingo") + (description "@acronym{Clorm, Clingo ORM} provides an @acronym{ORM, +Object Relational Mapping} interface to the @acronym{ASP, answer set +programming} solver clingo. Its goal is to make integration of clingo +into Python programs easier.") + (license license:expat))) + (define-public python-telingo (package (name "python-telingo") @@ -2749,6 +2905,41 @@ Python code."))) logic programs based on clingo.") (license license:expat))) +(define-public scasp + (let ((commit "89a427aa04ec6346425a40111c99b310901ffe51") + (revision "1")) + (package + (name "scasp") + (version (git-version "0.21.11.26" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/SWI-Prolog/sCASP") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1ijqv9xr3imrdmz6nq7zqwsmmaxn638icig19m8900m7mjfpizs4")))) + (build-system copy-build-system) + (arguments + (list + #:install-plan #~`(("scasp" "bin/") + ("prolog" "lib/swipl/library")) + #:modules `((guix build copy-build-system) + ((guix build gnu-build-system) #:prefix gnu:) + (guix build utils) + (ice-9 regex)) + #:phases + #~(modify-phases %standard-phases + (add-before 'install 'build (assoc-ref gnu:%standard-phases 'build)) + (add-after 'build 'check (assoc-ref gnu:%standard-phases 'check))))) + (native-inputs (list swi-prolog)) + (home-page "https://github.com/SWI-Prolog/sCASP") + (synopsis "Interpreter for ASP programs with constraints") + (description "@code{s(CASP)} is a top-down interpreter for ASP programs +with constraints.") + (license license:asl2.0)))) + (define-public ceres (package (name "ceres-solver") @@ -2968,61 +3159,6 @@ script files.") #t)))))) (synopsis "High-level language for numerical computation (with GUI)"))) -(define-public opencascade-oce - (package - (name "opencascade-oce") - (version "0.17.2") - (source - (origin - (method git-fetch) - (uri (git-reference - (url "https://github.com/tpaviot/oce") - (commit (string-append "OCE-" version)))) - (file-name (git-file-name name version)) - (patches (search-patches "opencascade-oce-glibc-2.26.patch")) - (sha256 - (base32 "0rg5wzkvfmzfl6v2amyryb8dnjad0nn9kyr607wy2gch6rciah69")))) - (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 - (list freetype - glu - libxmu - mesa - tcl - 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 opencascade-occt (package (name "opencascade-occt") @@ -3179,7 +3315,7 @@ This is the certified version of the Open Cascade Technology (OCCT) library.") (substitute* "api/gmsh.py" (("find_library\\(\"gmsh\"\\)") (simple-format #f "\"~a\"" libgmsh))))))))) - (home-page "http://gmsh.info/") + (home-page "https://gmsh.info/") (synopsis "3D finite element grid generator") (description "Gmsh is a 3D finite element grid generator with a built-in CAD engine and post-processor. Its design goal is to provide a fast, light @@ -3239,7 +3375,7 @@ ASCII text files using Gmsh's own scripting language.") (list ghostscript ;optional, for EPS/PS output python-dbus python-h5py ;optional, for HDF5 data - python-pyqt-without-qtwebkit + python-pyqt qtbase-5 qtsvg-5)) (propagated-inputs @@ -3703,7 +3839,7 @@ bindings to almost all functions of SLEPc.") (build-system gnu-build-system) (native-inputs (list autoconf automake)) - (home-page "http://us.metamath.org/") + (home-page "https://us.metamath.org/") (synopsis "Proof verifier based on a minimalistic formalism") (description "Metamath is a tiny formal language and that can express theorems in @@ -4382,7 +4518,7 @@ schemes.") #:phases (modify-phases %standard-phases (add-before 'check 'mpi-setup ,%openmpi-setup)))) - (home-page "http://www.p4est.org") + (home-page "https://www.p4est.org") (synopsis "Adaptive mesh refinement on forests of octrees") (description "The p4est software library enables the dynamic management of a @@ -4551,28 +4687,27 @@ point numbers.") (define-public wxmaxima (package (name "wxmaxima") - (version "22.05.0") - (source - (origin - (method git-fetch) - (uri (git-reference - (url "https://github.com/wxMaxima-developers/wxmaxima") - (commit (string-append "Version-" version)))) - (file-name (git-file-name name version)) - (sha256 - (base32 "1va56v9dys97yln4m1z3fz3k90lpy8i3kvcq0v1cbg36689aghm5")))) + (version "22.12.0") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/wxMaxima-developers/wxmaxima") + (commit (string-append "Version-" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "12bjadmy2mf7d8v4iszmzckahfcwjzaba8wpbigksh4brvhb4gj5")))) (build-system cmake-build-system) - (native-inputs - `(("gettext" ,gettext-minimal))) - (inputs - (list wxwidgets - maxima - ;; Runtime support. - adwaita-icon-theme - gtk+ - shared-mime-info)) + (native-inputs (list gettext-minimal)) + (inputs (list bash-minimal + wxwidgets + maxima + ;; Runtime support. + adwaita-icon-theme + gtk+ + shared-mime-info)) (arguments - `(#:tests? #f ; tests fail non-deterministically + `(#:tests? #f ; tests fail non-deterministically #:phases (modify-phases %standard-phases (add-after 'unpack 'patch-doc-path @@ -4581,8 +4716,8 @@ point numbers.") ;; documentation. Only licensing information is placed there by ;; Guix. (substitute* "src/Dirstructure.cpp" - (("/doc/wxmaxima-\\%s") "/doc/wxmaxima")) - #t)) + (("/doc/wxmaxima-\\%s") + "/doc/wxmaxima")))) (add-after 'install 'wrap-program (lambda* (#:key inputs outputs #:allow-other-keys) (wrap-program (string-append (assoc-ref outputs "out") @@ -4595,15 +4730,15 @@ point numbers.") (,(string-append (assoc-ref inputs "gtk+") "/share/glib-2.0/schemas"))) `("XDG_DATA_DIRS" ":" prefix - (;; Needed by gdk-pixbuf to know supported icon formats. - ,(string-append - (assoc-ref inputs "shared-mime-info") "/share") + ( ;; Needed by gdk-pixbuf to know supported icon formats. + ,(string-append (assoc-ref inputs "shared-mime-info") + "/share") ;; The default icon theme of GTK+. - ,(string-append - (assoc-ref inputs "adwaita-icon-theme") "/share")))) - #t))))) + ,(string-append (assoc-ref inputs "adwaita-icon-theme") + "/share"))))))))) (home-page "https://wxmaxima-developers.github.io/wxmaxima/") - (synopsis "Graphical user interface for the Maxima computer algebra system") + (synopsis + "Graphical user interface for the Maxima computer algebra system") (description "wxMaxima is a graphical user interface for the Maxima computer algebra system. It eases the use of Maxima by making most of its commands available @@ -4635,7 +4770,7 @@ full text searching.") `(("openblas" ,openblas) ("lapack" ,lapack) ("arpack" ,arpack-ng))) - (home-page "http://arma.sourceforge.net/") + (home-page "https://arma.sourceforge.net/") (synopsis "C++ linear algebra library") (description "Armadillo is a C++ linear algebra library, aiming towards a good balance @@ -5053,7 +5188,7 @@ Fresnel integrals, and similar related functions as well.") (native-inputs `(("cmake" ,cmake-minimal) ("m4" ,m4))) - (home-page "http://faculty.cse.tamu.edu/davis/suitesparse.html") + (home-page "https://faculty.cse.tamu.edu/davis/suitesparse.html") (synopsis "Suite of sparse matrix software") (description "SuiteSparse is a suite of sparse matrix algorithms, including: UMFPACK, @@ -5081,7 +5216,7 @@ packages.") (base32 "1dyjlq3fiparvm8ypwk6rsmjzmnwk81l88gkishphpvc79ryp216")))) (build-system gnu-build-system) - (home-page "http://math-atlas.sourceforge.net/") + (home-page "https://math-atlas.sourceforge.net/") (inputs `(("gfortran" ,gfortran) ("lapack-tar" ,(package-source lapack)))) (outputs '("out" "doc")) @@ -5337,7 +5472,7 @@ specifications.") (install-file name include)) (find-files "." "\\.h$"))) #t)))))) - (home-page "http://lpsolve.sourceforge.net/") + (home-page "https://lpsolve.sourceforge.net/") (synopsis "Mixed integer linear programming (MILP) solver") (description "lp_solve is a mixed integer linear programming solver based on the @@ -5684,7 +5819,7 @@ FLANN is written in C++ and contains bindings for C, Octave and Python.") (list mpfr readline)) (native-inputs (list bison flex)) - (home-page "http://w-calc.sourceforge.net/index.php") + (home-page "https://w-calc.sourceforge.net/index.php") (synopsis "Flexible command-line scientific calculator") (description "Wcalc is a very capable calculator. It has standard functions (sin, asin, and sinh for example, in either radians or degrees), many @@ -6083,6 +6218,177 @@ as equations, scalars, vectors, and matrices.") (home-page "https://www.gnu.org/software/jacal/") (license license:gpl3+))) +(define-public boolector + (package + (name "boolector") + (version "3.2.2") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/Boolector/boolector") + (commit version))) + (file-name (git-file-name name version)) + (patches (search-patches "boolector-find-googletest.patch")) + (sha256 + (base32 + "07rvp3iry7a7ixwl0q7nc47fwky1s1cyia7gqrjsg46syqlxbz2c")))) + (build-system cmake-build-system) + (arguments + (list #:configure-flags + #~(list "-DBUILD_SHARED_LIBS=on" + (string-append + "-DBtor2Tools_INCLUDE_DIR=" + (dirname (search-input-file %build-inputs + "include/btor2parser.h"))) + (string-append + "-DBtor2Tools_LIBRARIES=" + (search-input-file %build-inputs + "lib/libbtor2parser.so"))) + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'fix-cmake + (lambda _ + (delete-file "cmake/FindCryptoMiniSat.cmake") + (substitute* (list "CMakeLists.txt" "src/CMakeLists.txt") + (("find_package\\(CryptoMiniSat\\)") + "find_package(cryptominisat5 CONFIG) +find_package(louvain_communities)") + (("CryptoMiniSat_FOUND") "cryptominisat5_FOUND") + (("CryptoMiniSat_INCLUDE_DIR") + "CRYPTOMINISAT5_INCLUDE_DIRS") + (("CryptoMiniSat_LIBRARIES") + "CRYPTOMINISAT5_LIBRARIES")))) + (add-after 'unpack 'fix-sources + (lambda _ + (substitute* (find-files "." "\\.c$") + (("\"btor2parser/btor2parser\\.h\"") "<btor2parser.h>"))))))) + (inputs (list btor2tools + boost cryptominisat louvain-community sqlite)) + (native-inputs (list googletest pkg-config python-wrapper)) + (home-page "http://boolector.github.io/") + (synopsis "Bitvector-based theory solver") + (description "Boolector is a @acronym{SMT, satisfiability modulo theories} +solver for the theories of fixed-size bit-vectors, arrays and uninterpreted +functions.") + (license license:lgpl3+))) + +(define-public java-smtinterpol + (package + (name "java-smtinterpol") + (version "2.5") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/ultimate-pa/smtinterpol") + (commit version))) + (file-name (git-file-name name version)) + (modules '((guix build utils))) + (snippet #~(begin + (delete-file-recursively "jacoco") + (delete-file-recursively "libs") + (delete-file-recursively "sonar"))) + (sha256 + (base32 + "0bq5l7g830a8hxw1xyyfp2ph6jqk8ak0ichlymdglpnpngf6322f")))) + (build-system ant-build-system) + (arguments + (list #:build-target "dist" + #:test-target "runtests" + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'fix-build.xml + (lambda _ + (substitute* "build.xml" + (("<tstamp>") "<!--") + (("</tstamp>") "-->") + (("executable=\"git\"") + (string-append "executable=\"" + (which "sh") + "\"")) + (("<property file=.*/>" all) + (string-append all + "<property environment=\"env\" />")) + (("<classpath>" all) + (string-append + all + "<pathelement path=\"${env.CLASSPATH}\" />")) + (("<fileset file=\".*/libs/.*/>") "") + (("<junit") + "<junit haltonfailure=\"yes\"")) + (call-with-output-file "describe" + (lambda (port) + (format port "echo ~a" #$version))))) + (add-before 'check 'delete-failing-tests + (lambda _ + (delete-file + (string-append "SMTInterpolTest/src/de/uni_freiburg" + "/informatik/ultimate/smtinterpol/convert/" + "EqualityDestructorTest.java")))) + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (java (string-append out "/share/java"))) + (for-each (lambda (f) (install-file f java)) + (find-files "dist" "\\.jar$")))))))) + (native-inputs (list java-junit)) + (home-page "http://ultimate.informatik.uni-freiburg.de/smtinterpol/") + (synopsis "Interpolating SMT solver") + (description "SMTInterpol is an @acronym{SMT, Satisfiability Modulo Theories} +solver, that can compute Craig interpolants for various theories.") + (license license:lgpl3+))) + +(define-public yices + (package + (name "yices") + (version "2.6.4") + (source (origin + (method url-fetch) + (uri (string-append "https://yices.csl.sri.com/releases/" + version "/yices-" version "-src.tar.gz")) + (sha256 + (base32 + "1jvqvf35gv2dj936yzl8w98kc68d8fcdard90d6dddzc43h28fjk")))) + (build-system gnu-build-system) + (arguments + (list #:configure-flags + #~(list #$@(if (%current-target-system) + '() + (list (string-append "--build=" + (%current-system)))) + "--enable-mcsat" + ;; XXX: Ewww, static linkage + (string-append + "--with-static-libpoly=" + (search-input-file %build-inputs "lib/libpoly.a")) + (string-append + "--with-static-gmp=" + (search-input-file %build-inputs "lib/libgmp.a")) + (string-append + "--with-pic-libpoly=" + (search-input-file %build-inputs "lib/libpicpoly.a"))) + #:phases + #~(modify-phases %standard-phases + (add-after 'unpack 'fix-build-files + (lambda* (#:key outputs #:allow-other-keys) + (substitute* "Makefile.build" + (("SHELL=.*") "") + (("/sbin/ldconfig") (which "ldconfig"))) + (substitute* (find-files "etc" "install-yices.*") + (("/usr/bin/install") (which "install")) + (("/bin/ln") (which "ln")) + (("/sbin/ldconfig") (which "ldconfig")) + (("install_dir=.*") + (string-append "install_dir=" + (assoc-ref outputs "out"))))))))) + (inputs (list cudd gmp gperf libpoly)) + (native-inputs (list autoconf automake bash-minimal)) + (home-page "https://yices.csl.sri.com/") + (synopsis "Satisfiability modulo theories solver") + (description "Yices is a solver for @acronym{SMT, satisfiability modulo +theories} problems. It can process input in SMT-LIB format or its own +s-expression-based format.") + (license license:gpl3+))) + (define-public z3 (package (name "z3") @@ -7557,6 +7863,85 @@ generic reader and writer API.") (license (list license:expat license:bsd-3)))) ; blif2aig +(define-public btor2tools + (let ((commit "b8456dda4780789e882f5791eb486f295ade4da4") + (revision "1")) + (package + (name "btor2tools") + (version (git-version "1.0.0-pre" revision commit)) + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/Boolector/btor2tools") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0r3cm69q5xhnbxa74yvdfrsf349s4cxmiqlb4aq8appi7yg3qhww")))) + (build-system cmake-build-system) + (arguments + (list #:out-of-source? #f + #:phases + #~(modify-phases %standard-phases + (replace 'check + (lambda* (#:key tests? #:allow-other-keys) + (when tests? + (invoke "sh" "test/runtests.sh"))))))) + (home-page "http://boolector.github.io/") + (synopsis "Parser for BTOR2 format") + (description "This package provides a parser for the BTOR2 format used by +Boolector.") + (license license:lgpl3+)))) + +(define-public cudd + (package + (name "cudd") + (version "3.0.0") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/ivmai/cudd") + (commit (string-append "cudd-" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0hyw9q42ir92vcaa7bwv6f631n85rfsxp463rnmklniq1wf6dyn9")))) + (build-system gnu-build-system) + (arguments (list #:configure-flags #~(list "--enable-shared"))) + ;; The original home-page was lost to time, so we reference the "unofficial" + ;; Github mirror. For what it's worth, the author of the library appears to + ;; have been involved with this mirror at some point in time. + (home-page "https://github.com/ivmai/cudd") + (synopsis "Manipulate decision diagrams") + (description "@acronym{CUDD, Colorado University Decision Diagrams} is a +library for manipulating decision diagrams. It supports binary decision +diagrams, algebraic decision diagrams, and zero-suppressed binary decision +diagrams.") + (license license:bsd-3))) + +(define-public libpoly + (package + (name "libpoly") + (version "0.1.11") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/SRI-CSL/libpoly") + (commit (string-append "v" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0qylmg30rklvg00a0h1b3pb52cj9ki98yd27cylihjhq2klh3dmy")))) + (build-system cmake-build-system) + (arguments + (list #:configure-flags #~(list "-DLIBPOLY_BUILD_PYTHON_API=off"))) + (inputs (list gmp)) + (home-page "https://github.com/SRI-CSL/libpoly") + (synopsis "Manipulate polynomials") + (description "LibPoly is a C library for manipulating polynomials to support +symbolic reasoning engines that need to reason about polynomial constraints.") + (license license:lgpl3+))) + (define-public lingeling (let ((commit "72d2b13eea5fbd95557a3d0d199cd98dfbdc76ee") (revision "1")) @@ -7893,7 +8278,7 @@ numeric differences and differences in numeric formats.") (invoke "make" "byte") (invoke "make" "install-lib") #t))))) - (home-page "http://why3.lri.fr") + (home-page "https://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 @@ -7946,7 +8331,7 @@ of C, Java, or Ada programs.") (variable "FRAMAC_LIB") (files '("lib/frama-c")) (separator #f)))) - (home-page "http://frama-c.com") + (home-page "https://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 |