;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
+;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
;;;
;;; This file is part of GNU Guix.
;;;
(define-public petsc
(package
(name "petsc")
- (version "3.9.3")
+ (version "3.10.2")
(source
(origin
(method url-fetch)
(uri (string-append "http://ftp.mcs.anl.gov/pub/petsc/release-snapshots/"
"petsc-lite-" version ".tar.gz"))
(sha256
- (base32 "1fwkbwv4g7zf2lc8fw865xd0bl9anb6jaczfis5dff7h449gwa48"))))
+ (base32 "0bl64pydak3rblnjffi482r8bin4xim9sb37ksl2jkcxf0i0irsi"))))
(outputs '("out" ;libraries and headers
"examples")) ;~30MiB of examples
(build-system gnu-build-system)
(define-public slepc
(package
(name "slepc")
- (version "3.9.2")
+ (version "3.10.1")
(source
(origin
(method url-fetch)
version ".tar.gz"))
(sha256
(base32
- "0gmhdqac8zm3jx43h935z7bflazjnpvqxjv4jh5za2y1z2rqax94"))))
+ "188j1a133q91h8pivpnzwcf78kz8dvz2nzf6ndnjygdbqb48fizn"))))
(build-system gnu-build-system)
(native-inputs
`(("python" ,python-2)))
(lambda _
(chmod "src/maxima" #o555)
#t))
+ (replace 'check
+ (lambda _
+ ;; This is derived from the testing code in the "debian/rules" file
+ ;; of Debian's Maxima package.
+ ;; If Maxima can successfully run this, the binary to be installed
+ ;; should be fine.
+ (zero?
+ (system
+ (string-append "./maxima-local "
+ "--lisp=gcl "
+ "--batch-string=\"run_testsuite();\" "
+ "| grep -q \"No unexpected errors found\"")))))
;; 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.
(define-public z3
(package
(name "z3")
- (version "4.5.0")
+ (version "4.8.1")
+ (home-page "https://github.com/Z3Prover/z3")
(source (origin
- (method url-fetch)
- (uri (string-append
- "https://github.com/Z3Prover/z3/archive/z3-"
- version ".tar.gz"))
+ (method git-fetch)
+ (uri (git-reference (url home-page)
+ (commit (string-append "z3-" version))))
(sha256
(base32
- "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
+ "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f"))))
(build-system cmake-build-system)
(arguments
`(#:configure-flags
(synopsis "Theorem prover")
(description "Z3 is a theorem prover and @dfn{satisfiability modulo
theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.")
- (home-page "https://github.com/Z3Prover/z3")
(license license:expat)))
(define-public cubicle
(package
(name "cubicle")
- (version "1.1.1")
+ (version "1.1.2")
(source (origin
(method url-fetch)
(uri (string-append "http://cubicle.lri.fr/cubicle-"
version ".tar.gz"))
(sha256
(base32
- "1sny9c4fm14k014pk62ibpwbrjjirkx8xmhs9jg7q1hk7y7x3q2h"))))
+ "10kk80jdmpdvql88sdjsh7vqzlpaphd8vip2lp47aarxjkwjlz1q"))))
(build-system gnu-build-system)
(native-inputs
- `(("ocaml" ,ocaml)
+ `(("automake" ,automake)
+ ("ocaml" ,ocaml)
("which" ,(@@ (gnu packages base) which))))
(propagated-inputs
- `(("z3" ,z3)))
+ `(("ocaml-num" ,ocaml-num)
+ ("z3" ,z3)))
(arguments
`(#:configure-flags (list "--with-z3")
+ #:make-flags (list "QUIET=")
#:tests? #f
#:phases
(modify-phases %standard-phases
(add-before 'configure 'configure-for-release
(lambda _
(substitute* "Makefile.in"
- (("SVNREV=") "#SVNREV="))))
+ (("SVNREV=") "#SVNREV="))
+ #t))
(add-before 'configure 'fix-/bin/sh
(lambda _
(substitute* "configure"
- (("/bin/sh") (which "sh")))))
+ (("-/bin/sh") (string-append "-" (which "sh"))))
+ #t))
(add-before 'configure 'fix-smt-z3wrapper.ml
(lambda _
(substitute* "Makefile.in"
- (("\\\\n") "")))))))
+ (("\\\\n") ""))
+ #t))
+ (add-before 'configure 'fix-ocaml-num
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* "Makefile.in"
+ (("= \\$\\(FUNCTORYLIB\\)")
+ (string-append "= -I "
+ (assoc-ref inputs "ocaml-num")
+ "/lib/ocaml/site-lib"
+ " $(FUNCTORYLIB)")))
+ #t)))))
(home-page "http://cubicle.lri.fr/")
(synopsis "Model checker for array-based systems")
(description "Cubicle is a model checker for verifying safety properties