remove pushed z3
more/packages/smt.scm
23 | 23 | #:use-module (guix build-system python) | |
24 | 24 | #:use-module ((guix licenses) #:prefix license:) | |
25 | 25 | #:use-module (gnu packages) | |
26 | + | #:use-module (gnu packages maths) | |
26 | 27 | #:use-module (gnu packages ocaml) | |
27 | 28 | #:use-module (gnu packages python) | |
28 | 29 | #:use-module (more packages python)) | |
29 | 30 | ||
30 | - | (define-public z3-solver | |
31 | - | (package | |
32 | - | (name "z3-solver") | |
33 | - | (version "4.5.0") | |
34 | - | (source (origin | |
35 | - | (method url-fetch) | |
36 | - | (uri (string-append "https://github.com/Z3Prover/z3/archive/z3-" | |
37 | - | version ".tar.gz")) | |
38 | - | (sha256 | |
39 | - | (base32 | |
40 | - | "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf")) | |
41 | - | (file-name (string-append name "-" version ".tar.gz")))) | |
42 | - | (build-system gnu-build-system) | |
43 | - | (arguments | |
44 | - | `(#:phases | |
45 | - | (modify-phases %standard-phases | |
46 | - | (delete 'configure) | |
47 | - | (add-before 'build 'generate-make | |
48 | - | (lambda _ | |
49 | - | (system* "python" "scripts/mk_make.py") | |
50 | - | (chdir "build")))) | |
51 | - | #:test-target "test" | |
52 | - | #:make-flags | |
53 | - | (list (string-append "PREFIX=" (assoc-ref %outputs "out"))))) | |
54 | - | (native-inputs | |
55 | - | `(("python" ,python-2))) | |
56 | - | (home-page "https://github.com/Z3Prover/z3") | |
57 | - | (synopsis "SMT solver library") | |
58 | - | (description "Z3 is a theorem prover from Microsoft Research.") | |
59 | - | (license license:expat))) | |
60 | - | ||
61 | 31 | (define-public python2-z3-solver | |
62 | 32 | (package | |
63 | - | (inherit z3-solver) | |
33 | + | (inherit z3) | |
64 | 34 | (name "python2-z3-solver") | |
65 | 35 | (build-system python-build-system) | |
66 | 36 | (propagated-inputs | |
67 | - | `(("z3" ,z3-solver))) | |
37 | + | `(("z3" ,z3))) | |
68 | 38 | (arguments | |
69 | 39 | `(#:python ,python-2 | |
70 | 40 | #:phases |