From 3366be5db0d744625accc80ebc8d155bf1ddece8 Mon Sep 17 00:00:00 2001
From: Zhu Zihao <all_but_last@163.com>
Date: Mon, 20 Jun 2022 20:09:20 +0800
Subject: [PATCH] gnu: z3: Use G-expressions.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

Signed-off-by: Ludovic Courtès <ludo@gnu.org>
---
 gnu/packages/maths.scm | 89 +++++++++++++++++++++---------------------
 1 file 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 @@ (define-public z3
                 "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.")