me/guix
Archived
1
0
Fork 0
Code Activity

gnu: z3: Use G-expressions.

Browse source 
* gnu/packages/maths.scm (z3)[arguments]: Use G-expressions.
[native-inputs]: Use label-less style.

Signed-off-by: Ludovic Courtès <ludo@gnu.org>
This commit is contained in:
Zhu Zihao 2022-06-20 20:09:20 +08:00 • committed by Ludovic Courtès
parent 7cddd130df
commit 3366be5db0
No known key found for this signature in database
GPG key ID: 090B11993D9AEBB5
1 changed files with 45 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

89
gnu/packages/maths.scm
View file

@ -50,6 +50,7 @@
;;; Copyright © 2021 Jean-Baptiste Volatier <jbv@pm.me> ;;; Copyright © 2021 Jean-Baptiste Volatier <jbv@pm.me>
;;; Copyright © 2021 Guillaume Le Vaillant <glv@posteo.net> ;;; Copyright © 2021 Guillaume Le Vaillant <glv@posteo.net>
;;; Copyright © 2021 Pierre-Antoine Bouttier <pierre-antoine.bouttier@univ-grenoble-alpes.fr> ;;; 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. ;;; This file is part of GNU Guix.
;;; ;;;
@ -5831,51 +5832,51 @@ as equations, scalars, vectors, and matrices.")
"1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx")))) "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"))))
(build-system gnu-build-system) (build-system gnu-build-system)
(arguments (arguments
`(#:imported-modules ((guix build python-build-system) (list
,@%gnu-build-system-modules) #:imported-modules `((guix build python-build-system)
#:modules (((guix build python-build-system) #:select (site-packages)) ,@%cmake-build-system-modules)
(guix build gnu-build-system) #:modules '((guix build cmake-build-system)
(guix build utils)) (guix build utils)
#:phases ((guix build python-build-system) #:select (site-packages)))
(modify-phases %standard-phases #:phases
(add-after 'unpack 'enable-bytecode-determinism #~(modify-phases %standard-phases
(lambda _ (add-after 'unpack 'enable-bytecode-determinism
(setenv "PYTHONHASHSEED" "0") (lambda _
#t)) (setenv "PYTHONHASHSEED" "0")
(add-after 'unpack 'fix-compatability #t))
;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only. (add-after 'unpack 'fix-compatability
(lambda _ ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows only.
(substitute* "src/util/mpz.cpp" (lambda _
(("#include <immintrin.h>") "")) (substitute* "src/util/mpz.cpp"
#t)) (("#include <immintrin.h>") ""))
(add-before 'configure 'bootstrap #t))
(lambda _ (add-before 'configure 'bootstrap
(invoke "python" "scripts/mk_make.py"))) (lambda _
;; work around gnu-build-system's setting --enable-fast-install (invoke "python" "scripts/mk_make.py")))
;; (z3's `configure' is a wrapper around the above python file, ;; work around gnu-build-system's setting --enable-fast-install
;; which fails when passed --enable-fast-install) ;; (z3's `configure' is a wrapper around the above python file,
(replace 'configure ;; which fails when passed --enable-fast-install)
(lambda* (#:key inputs outputs #:allow-other-keys) (replace 'configure
(invoke "./configure" (lambda* (#:key inputs outputs #:allow-other-keys)
"--python" (invoke "./configure"
(string-append "--prefix=" (assoc-ref outputs "out")) "--python"
(string-append "--pypkgdir=" (site-packages inputs outputs))))) (string-append "--prefix=" (assoc-ref outputs "out"))
(add-after 'configure 'change-directory (string-append "--pypkgdir=" (site-packages inputs outputs)))))
(lambda _ (add-after 'configure 'change-directory
(chdir "build") (lambda _
#t)) (chdir "build")
(add-before 'check 'make-test-z3 #t))
(lambda _ (add-before 'check 'make-test-z3
;; Build the test suite executable. (lambda _
(invoke "make" "test-z3" "-j" ;; Build the test suite executable.
(number->string (parallel-job-count))))) (invoke "make" "test-z3" "-j"
(replace 'check (number->string (parallel-job-count)))))
(lambda _ (replace 'check
;; Run all the tests that don't require arguments. (lambda _
(invoke "./test-z3" "/a")))))) ;; Run all the tests that don't require arguments.
(invoke "./test-z3" "/a"))))))
(native-inputs (native-inputs
`(("which" ,which) (list which python-wrapper))
("python" ,python-wrapper)))
(synopsis "Theorem prover") (synopsis "Theorem prover")
(description "Z3 is a theorem prover and @dfn{satisfiability modulo (description "Z3 is a theorem prover and @dfn{satisfiability modulo
theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.") theories} (SMT) solver. It provides a C/C++ API, as well as Python bindings.")