From 313844d9dc098b44cd27dcfa1a26de306c9a8fe2 Mon Sep 17 00:00:00 2001 From: Theodoros Foradis Date: Tue, 25 Jul 2017 19:11:12 +0300 Subject: gnu: Add z3. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/maths.scm (z3): New variable. Signed-off-by: Ludovic Courtès --- gnu/packages/maths.scm | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'gnu/packages') diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 7d4cb45b18..6566d750b2 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -18,6 +18,7 @@ ;;; Copyright © 2017 Paul Garlick ;;; Copyright © 2017 ng0 ;;; Copyright © 2017 Ben Woodcroft +;;; Copyright © 2017 Theodoros Foradis ;;; ;;; This file is part of GNU Guix. ;;; @@ -3161,3 +3162,37 @@ as equations, scalars, vectors, and matrices.") (home-page "https://www.gnu.org/software/jacal/") (license license:gpl3+))) +(define-public z3 + (package + (name "z3") + (version "4.5.0") + (source (origin + (method url-fetch) + (uri (string-append + "https://github.com/Z3Prover/z3/archive/z3-" + version ".tar.gz")) + (sha256 + (base32 + "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")))) + (build-system gnu-build-system) + (arguments + `(#:test-target "test" + #:phases + (modify-phases %standard-phases + (replace 'configure + (lambda* (#:key inputs outputs #:allow-other-keys) + (zero? + (system* "python" "scripts/mk_make.py" + (string-append "--prefix=" + (assoc-ref outputs "out")))))) + (add-after 'configure 'change-dir + (lambda _ + (chdir "build") + #t))))) + (native-inputs + `(("python" ,python-2))) + (synopsis "Theorem prover") + (description "Z3 is a theorem prover and @dfn{satisfiability modulo +theories} (SMT) solver. It provides a C/C++ API.") + (home-page "https://github.com/Z3Prover/z3") + (license license:expat))) -- cgit v1.2.3 lass='list nowrap'>AgeCommit message (Expand)Author 2024-04-15utils: Don’t re-export ‘call-with-temporary-output-file’....* guix/utils.scm: Remove re-export of ‘call-with-temporary-output-file’. Autoload a number of modules. * guix/download.scm, guix/import/hackage.scm, guix/import/hexpm.scm, guix/import/opam.scm, guix/import/pypi.scm, tests/cpio.scm, tests/egg.scm, tests/opam.scm, tests/publish.scm, tests/store-database.scm, tests/utils.scm: Adjust imports accordingly. Change-Id: I3f5e94631397996a30be2ea4ff8b50a3371e8ee7 Ludovic Courtès 2024-02-23utils: Add find-definition-insertion-location procedure....* guix/utils.scm (find-definition-insertion-location): Add and export procedure. * tests/utils.scm ("find-definition-insertion-location"): Add test. Change-Id: Ie17e1b4a94790f58518ce121411a38d357f49feb Signed-off-by: Ludovic Courtès <ludo@gnu.org> Herman Rimm 2024-02-23utils: Add insert-expression procedure....* guix/utils.scm (define-module): Use (guix read-print) and export (insert-expression). (insert-expression): Add procedure. * tests/utils.scm ("insert-expression"): Add test. Change-Id: I971a43a78aa6ecaaef33c1a7a0db4b287eb85036 Signed-off-by: Ludovic Courtès <ludo@gnu.org> Herman Rimm 2023-12-11guix: Add target-avr?....* guix/utils.scm (target-avr?): New procedure. * tests/utils.scm: Add tests for target-avr? procedure. Change-Id: Iaa0fa97a2b6bc45d45f907f43157f1548a0ba3fa Signed-off-by: Efraim Flashner <efraim@flashner.co.il> Jean-Pierre De Jesus DIAZ 2021-07-14utils: Define a target-x86-32? and target-x86-64? predicate....* guix/utils.scm (target-x86-32?, target-x86-64?): New predicates. * tests/utils.scm ("target-x86-32?", "target-x86-64?"): New tests. Signed-off-by: Mathieu Othacehe <othacehe@gnu.org> Maxime Devos 2021-07-14utils: Define 'target-linux?' predicate....* guix/utils.scm (target-linux?): New predicate. * tests/utils.scm ("target-linux?"): Test it. ("target-mingw?"): Also test ‘target-mingw?’. Signed-off-by: Mathieu Othacehe <othacehe@gnu.org> Maxime Devos 2021-02-03utils: Add string distance....* guix/utils.scm (string-distance): New procedure. (string-closest): New procedure. * tests/utils.scm ("string-distance", "string-closest"): New tests. Signed-off-by: Ludovic Courtès <ludo@gnu.org> zimoun 2021-02-01utils: Add 'version-unique-prefix'....* guix/utils.scm (version-unique-prefix): New procedure. * tests/utils.scm ("version-unique-prefix"): New test. Ludovic Courtès 2021-01-13utils: Support zstd compression via Guile-zstd....* guix/utils.scm (lzip-port): Return a single value. (zstd-port): New procedure. (decompressed-port, compressed-output-port): Add 'zstd' case. * tests/utils.scm (test-compression/decompression): Test 'zstd' when the (zstd) module is available. Ludovic Courtès 2021-01-13utils: Remove 'compressed-output-port'....This procedure was unused except in one test. * guix/utils.scm (compressed-port): Remove. * tests/utils.scm (test-compression/decompression): Rewrite to use 'compressed-output-port' instead. Ludovic Courtès 2020-08-24Use "guile-zlib" and "guile-lzlib" instead of (guix config)....* Makefile.am (MODULES): Remove guix/zlib.scm and guix/lzlib.scm, (SCM_TESTS): remove tests/zlib.scm, tests/lzlib.scm. * build-aux/build-self.scm (make-config.scm): Remove unused %libz variable. * configure.ac: Remove LIBZ and LIBLZ variables and check instead for Guile-zlib and Guile-lzlib. * doc/guix.texi ("Requirements"): Remove zlib requirement and add Guile-zlib and Guile-lzlib instead. * gnu/packages/package-management.scm (guix)[native-inputs]: Add "guile-zlib" and "guile-lzlib", [inputs]: remove "zlib" and "lzlib", [propagated-inputs]: ditto, [arguments]: add "guile-zlib" and "guile-lzlib" to Guile load path. * guix/config.scm.in (%libz, %liblz): Remove them. * guix/lzlib.scm: Remove it. * guix/man-db.scm: Use (zlib) instead of (guix zlib). * guix/profiles.scm (manual-database): Do not stub (guix config) in imported modules list, instead add "guile-zlib" to the extension list. * guix/scripts/publish.scm: Use (zlib) instead of (guix zlib) and (lzlib) instead of (guix lzlib), (string->compression-type, effective-compression): do not check for zlib and lzlib availability. * guix/scripts/substitute.scm (%compression-methods): Do not check for lzlib availability. * guix/self.scm (specification->package): Add "guile-zlib" and "guile-lzlib" and remove "zlib" and "lzlib", (compiled-guix): remove "zlib" and "lzlib" arguments and add guile-zlib and guile-lzlib to the dependencies, also do not pass "zlib" and "lzlib" to "make-config.scm" procedure, (make-config.scm): remove "zlib" and "lzlib" arguments as well as %libz and %liblz variables. * guix/utils.scm (lzip-port): Use (lzlib) instead of (guix lzlib) and do not check for lzlib availability. * guix/zlib.scm: Remove it. * m4/guix.m4 (GUIX_LIBZ_LIBDIR, GUIX_LIBLZ_FILE_NAME): Remove them. * tests/lzlib.scm: Use (zlib) instead of (guix zlib) and (lzlib) instead of (guix lzlib), and do not check for zlib and lzlib availability. * tests/publish.scm: Ditto. * tests/substitute.scm: Do not check for lzlib availability. * tests/utils.scm: Ditto. * tests/zlib.scm: Remove it. Mathieu Othacehe