ryan77627/guix
1
0
Fork 0
mirror of https://git.in.rschanz.org/ryan77627/guix.git synced 2024-11-07 23:46:13 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

gnu: z3: Prefer CMake to build the package.

Browse source 
Z3 developer recommends to use CMake to build Z3 except the OCaml bindings.
Use CMake also enable us to cross compile z3.

* gnu/packages/maths.scm (z3)[build-system]: Use cmake-build-system.
[arguments]<#:configure-flags>: Add flags for CMake.
<#:phases>: Remove stale phase 'fix-compatability'.
In phase 'check', build the z3 test binary and don't test when cross
compiling.
Add phase 'compile-python-modules' phase to generate python bytecode cache for
z3 python binding.
Add phase 'fix-z3-library-path' to help z3 pythong binding to find the z3
shared library.

(ocaml-z3)[build-system]: Override the inherited value with 'gnu-build-system'.

Signed-off-by: Ludovic Courtès <ludo@gnu.org>
This commit is contained in:
Zhu Zihao 2022-06-20 20:17:54 +08:00 committed by Ludovic Courtès
parent cec5142183
commit 0e64835b2e
No known key found for this signature in database
GPG key ID: 090B11993D9AEBB5
1 changed files with 31 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
gnu/packages/maths.scm
View file

@ -5829,8 +5829,8 @@ (define-public z3
(file-name (git-file-name name version))
(sha256
(base32
(build-system gnu-build-system)
"1vvb09q7w7zd29qc4qjysrrhyylszm1wf6azkff004ixwn026b05"))))
(build-system cmake-build-system)
(arguments
(list
#:imported-modules `((guix build python-build-system)
@ -5838,43 +5838,40 @@ (define-public z3
#:modules '((guix build cmake-build-system)
(guix build utils)
((guix build python-build-system) #:select (site-packages)))
#:configure-flags
#~(list "-DZ3_BUILD_PYTHON_BINDINGS=ON"
"-DZ3_LINK_TIME_OPTIMIZATION=ON"
(string-append
"-DCMAKE_INSTALL_PYTHON_PKG_DIR="
#$output "/lib/python"
#$(version-major+minor (package-version python-wrapper))
"/site-packages"))
#:phases
#~(modify-phases %standard-phases
(add-after 'unpack 'enable-bytecode-determinism
(replace 'check
(lambda* (#:key parallel-build? tests? #:allow-other-keys)
(when tests?
(invoke "make" "test-z3"
(format #f "-j~a"
(if parallel-build?
(parallel-job-count)
1)))
(invoke "./test-z3" "/a"))))
(add-after 'install 'compile-python-modules
(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
(invoke "python" "-m" "compileall"
"--invalidation-mode=unchecked-hash"
#$output)))
;; This step is missing in the CMake build system, do it here.
(add-after 'compile-python-modules 'fix-z3-library-path
(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"))))))
(let* ((dest (string-append (site-packages inputs outputs)
"/z3/lib/libz3.so"))
(z3-lib (string-append #$output "/lib/libz3.so")))
(mkdir-p (dirname dest))
(symlink z3-lib dest)))))))
(native-inputs
(list which python-wrapper))
(synopsis "Theorem prover")
@ -5886,6 +5883,7 @@ (define-public ocaml-z3
(package
(inherit z3)
(name "ocaml-z3")
(build-system gnu-build-system)
(arguments
`(#:imported-modules ((guix build python-build-system)
,@%gnu-build-system-modules)