summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorZhu Zihao <all_but_last@163.com>2022-06-20 20:09:20 +0800
committerLudovic Courtès <ludo@gnu.org>2022-07-04 12:29:04 +0200
commit3366be5db0d744625accc80ebc8d155bf1ddece8 (patch)
tree0ac4a05e623afa6a1da00cc826ebbff5b6c701fd
parent7cddd130df4c7e872ff05693b24643302adcbbc7 (diff)
downloadguix-3366be5db0d744625accc80ebc8d155bf1ddece8.tar.gz
guix-3366be5db0d744625accc80ebc8d155bf1ddece8.tar.xz
gnu: z3: Use G-expressions.
* gnu/packages/maths.scm (z3)[arguments]: Use G-expressions. [native-inputs]: Use label-less style. Signed-off-by: Ludovic Courtès <ludo@gnu.org>
-rw-r--r--gnu/packages/maths.scm89
1 files changed, 45 insertions, 44 deletions
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index e84697c63b..945795a055 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -50,6 +50,7 @@
;;; Copyright © 2021 Jean-Baptiste Volatier <jbv@pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv@posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier@univ-grenoble-alpes.fr>
+;;; Copyright © 2022 Zhu Zihao <all_but_last@163.com>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -5831,51 +5832,51 @@ as equations, scalars, vectors, and matrices.")
"1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system)
(arguments
- `(#:imported-modules ((guix build python-build-system)
- ,@%gnu-build-system-modules)
- #:modules (((guix build python-build-system) #:select (site-packages))
- (guix build gnu-build-system)
- (guix build utils))
- #:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'enable-bytecode-determinism
- (lambda _
- (setenv "PYTHONHASHSEED" "0")
- #t))
- (add-after 'unpack 'fix-compatability
- ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
- (lambda _
- (substitute* "src/util/mpz.cpp"
- (("#include <immintrin.h>") ""))
- #t))
- (add-before 'configure 'bootstrap
- (lambda _
- (invoke "python" "scripts/mk_make.py")))
- ;; work around gnu-build-system's setting --enable-fast-install
- ;; (z3's `configure' is a wrapper around the above python file,
- ;; which fails when passed --enable-fast-install)
- (replace 'configure
- (lambda* (#:key inputs outputs #:allow-other-keys)
- (invoke "./configure"
- "--python"
- (string-append "--prefix=" (assoc-ref outputs "out"))
- (string-append "--pypkgdir=" (site-packages inputs outputs)))))
- (add-after 'configure 'change-directory
- (lambda _
- (chdir "build")
- #t))
- (add-before 'check 'make-test-z3
- (lambda _
- ;; Build the test suite executable.
- (invoke "make" "test-z3" "-j"
- (number->string (parallel-job-count)))))
- (replace 'check
- (lambda _
- ;; Run all the tests that don't require arguments.
- (invoke "./test-z3" "/a"))))))
+ (list
+ #:imported-modules `((guix build python-build-system)
+ ,@%cmake-build-system-modules)
+ #:modules '((guix build cmake-build-system)
+ (guix build utils)
+ ((guix build python-build-system) #:select (site-packages)))
+ #:phases
+ #~(modify-phases %standard-phases
+ (add-after 'unpack 'enable-bytecode-determinism
+ (lambda _
+ (setenv "PYTHONHASHSEED" "0")
+ #t))
+ (add-after 'unpack 'fix-compatability
+ ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
+ (lambda _
+ (substitute* "src/util/mpz.cpp"
+ (("#include <immintrin.h>") ""))
+ #t))
+ (add-before 'configure 'bootstrap
+ (lambda _
+ (invoke "python" "scripts/mk_make.py")))
+ ;; work around gnu-build-system's setting --enable-fast-install
+ ;; (z3's `configure' is a wrapper around the above python file,
+ ;; which fails when passed --enable-fast-install)
+ (replace 'configure
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (invoke "./configure"
+ "--python"
+ (string-append "--prefix=" (assoc-ref outputs "out"))
+ (string-append "--pypkgdir=" (site-packages inputs outputs)))))
+ (add-after 'configure 'change-directory
+ (lambda _
+ (chdir "build")
+ #t))
+ (add-before 'check 'make-test-z3
+ (lambda _
+ ;; Build the test suite executable.
+ (invoke "make" "test-z3" "-j"
+ (number->string (parallel-job-count)))))
+ (replace 'check
+ (lambda _
+ ;; Run all the tests that don't require arguments.
+ (invoke "./test-z3" "/a"))))))
(native-inputs
- `(("which" ,which)
- ("python" ,python-wrapper)))
+ (list which python-wrapper))
(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.")