z3: 4.6.0 -> 4.7.1 #41068

dtzWill · 2018-05-25T02:14:50Z

Update!

Needs testing,
not sure how many rebuilds this'll trigger
or if apps will generally be compat or not.

Tested using sandboxing (nix.useSandbox on NixOS, or option build-use-sandbox in nix.conf on non-NixOS)
Built on platform(s)
- NixOS
- macOS
- other Linux distributions
Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
Tested execution of all binary files (usually in ./result/bin/)
Fits CONTRIBUTING.md.

GrahamcOfBorg · 2018-05-25T02:29:36Z

Success on aarch64-linux (full log)

Attempted: z3

Partial log (click to expand)

Z3Py was installed at /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1/lib/python2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1
shrinking /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1/lib/libz3.so
shrinking /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1/bin/z3
strip is /nix/store/jk6j4lh9v5mvjdbdc35sj0zffhhf6s56-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1/lib  /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1/bin
patching script interpreter paths in /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1
checking for references to /build in /nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1...
/nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1

GrahamcOfBorg · 2018-05-25T02:30:42Z

Success on x86_64-darwin (full log)

Attempted: z3

Partial log (click to expand)

clang++ -o libz3.dylib -dynamiclib api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/dll/dll.o api/api_array.o api/api_fpa.o api/api_arith.o api/api_interp.o api/api_datatype.o api/z3_replayer.o api/api_model.o api/api_log_macros.o api/api_ast_map.o api/api_datalog.o api/api_ast_vector.o api/api_commands.o api/api_opt.o api/api_algebraic.o api/api_tactic.o api/api_ast.o api/api_context.o api/api_qe.o api/api_log.o api/api_pb.o api/api_polynomial.o api/api_goal.o api/api_rcf.o api/api_seq.o api/api_bv.o api/api_stats.o api/api_config_params.o api/api_solver.o api/api_quant.o api/api_params.o api/api_numeral.o api/api_parsers.o opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a ast/proofs/proofs.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a
cp libz3.dylib python
Z3Py was installed at /nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1/lib/python2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
post-installation fixup
strip is /nix/store/kdff2gim6417493yha769kh00n63lnrw-cctools-binutils-darwin/bin/strip
stripping (with command strip and flags -S) in /nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1/lib  /nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1/bin
patching script interpreter paths in /nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1
/nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1/lib/python2.7/site-packages/z3/lib/libz3.dylib: fixing dylib
/nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1/lib/libz3.dylib: fixing dylib
/nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1

GrahamcOfBorg · 2018-05-25T02:31:01Z

Success on x86_64-linux (full log)

Attempted: z3

Partial log (click to expand)

Z3Py was installed at /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1/lib/python2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1
shrinking /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1/bin/z3
shrinking /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1/lib/libz3.so
strip is /nix/store/j75dgadrff2d1fyc4fczmcgqkid2imdx-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1/lib  /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1/bin
patching script interpreter paths in /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1
checking for references to /build in /nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1...
/nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1

Mic92 · 2018-05-25T10:59:26Z

@GrahamcOfBorg build haskellPackages.sbvPlugin haskellPackages.z3 haskellPackages.copilot-sbv cryptol haskellPackages.ntha solc dotnetPackages.Dafny seth dotnetPackages.Boogie boogie z3 haskellPackages.linearEqSolver souper fstar haskellPackages.cryptol tlaps isabelle haskellPackages.sbv cuter haskellPackages.ez3 dafny altcoins.seth

Mic92 · 2018-05-25T10:59:52Z

Does not look like it has too many users.

Mic92 · 2018-05-25T11:01:58Z

Seems non-critical: https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES#L3

GrahamcOfBorg · 2018-05-25T11:30:56Z

Failure on x86_64-darwin (full log)

Attempted: haskellPackages.sbvPlugin, haskellPackages.z3, haskellPackages.copilot-sbv, cryptol, haskellPackages.ntha, solc, dotnetPackages.Dafny, seth, dotnetPackages.Boogie, boogie, z3, haskellPackages.linearEqSolver, fstar, haskellPackages.cryptol, haskellPackages.sbv, cuter, haskellPackages.ez3, dafny, altcoins.seth

The following builds were skipped because they don't evaluate on x86_64-darwin: souper, tlaps, isabelle

Partial log (click to expand)

[ 67%] Building CXX object lib/CodeGen/CMakeFiles/LLVMCodeGen.dir/TargetPassConfig.cpp.o
[ 67%] Building CXX object lib/Target/AArch64/CMakeFiles/LLVMAArch64CodeGen.dir/AArch64CallLowering.cpp.o
[ 68%] Building CXX object lib/Target/ARM/CMakeFiles/LLVMARMCodeGen.dir/ARMLoadStoreOptimizer.cpp.o
[ 68%] Building CXX object lib/Target/AArch64/CMakeFiles/LLVMAArch64CodeGen.dir/AArch64CleanupLocalDynamicTLSPass.cpp.o
[ 68%] Building CXX object lib/Target/AArch64/CMakeFiles/LLVMAArch64CodeGen.dir/AArch64CollectLOH.cpp.o
building of '/nix/store/dvfcr5b362ymixjjc4xcyvv7j877f89z-rustc-1.25.0.drv' timed out after 1800 seconds
cannot build derivation '/nix/store/kn2f0scghqixqhh1zdkd6arl9wmyx0h5-cargo-0.26.0.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/ijvnf82l6plcnvj9g5y1q8kmvisbf962-ethabi-4.1.0.drv': 2 dependencies couldn't be built
cannot build derivation '/nix/store/9bklxn5fh10qkvl9kca7rlw0ygilaqwy-seth-0.6.3.drv': 1 dependencies couldn't be built
�[31;1merror:�[0m build of '/nix/store/0sfjn8051k34yran0kzi9qf9cbvfjdw6-Boogie-unstable-2017-01-03.drv', '/nix/store/2d87z5dbcn6makyq0wqglx0m689w3mnk-Dafny-2.1.0.drv', '/nix/store/9bklxn5fh10qkvl9kca7rlw0ygilaqwy-seth-0.6.3.drv' failed

GrahamcOfBorg · 2018-05-25T11:32:15Z

Failure on x86_64-linux (full log)

Attempted: haskellPackages.sbvPlugin, haskellPackages.z3, haskellPackages.copilot-sbv, cryptol, haskellPackages.ntha, solc, dotnetPackages.Dafny, seth, dotnetPackages.Boogie, boogie, z3, haskellPackages.linearEqSolver, souper, fstar, haskellPackages.cryptol, tlaps, isabelle, haskellPackages.sbv, cuter, haskellPackages.ez3, dafny, altcoins.seth

Partial log (click to expand)

wrong ELF type
shrinking RPATHs of ELF executables and libraries in /nix/store/d5w5fcr1v2k85a0w18mp0qkbfisa4xb4-ntha-0.1.3-data
strip is /nix/store/j75dgadrff2d1fyc4fczmcgqkid2imdx-binutils-2.30/bin/strip
patching script interpreter paths in /nix/store/d5w5fcr1v2k85a0w18mp0qkbfisa4xb4-ntha-0.1.3-data
checking for references to /build in /nix/store/d5w5fcr1v2k85a0w18mp0qkbfisa4xb4-ntha-0.1.3-data...
shrinking RPATHs of ELF executables and libraries in /nix/store/kf16wshymkwbq5i04fhhzfbwp8ys1hpy-ntha-0.1.3-doc
strip is /nix/store/j75dgadrff2d1fyc4fczmcgqkid2imdx-binutils-2.30/bin/strip
patching script interpreter paths in /nix/store/kf16wshymkwbq5i04fhhzfbwp8ys1hpy-ntha-0.1.3-doc
checking for references to /build in /nix/store/kf16wshymkwbq5i04fhhzfbwp8ys1hpy-ntha-0.1.3-doc...
error: build of '/nix/store/q1r6aljqqm4ar9y9x7pi1rrhf04l2r4p-Boogie-unstable-2017-01-03.drv', '/nix/store/rwq7xr2vqm781j0mmas8x225qh1vfczz-Dafny-2.1.0.drv' failed

GrahamcOfBorg · 2018-05-25T11:47:27Z

Failure on aarch64-linux (full log)

Attempted: solc, dotnetPackages.Dafny, seth, dotnetPackages.Boogie, boogie, z3, souper, fstar, cuter, dafny, altcoins.seth

The following builds were skipped because they don't evaluate on aarch64-linux: haskellPackages.sbvPlugin, haskellPackages.z3, haskellPackages.copilot-sbv, cryptol, haskellPackages.ntha, haskellPackages.linearEqSolver, haskellPackages.cryptol, tlaps, isabelle, haskellPackages.sbv, haskellPackages.ez3

Partial log (click to expand)

make[2]: Leaving directory '/build/mono-5.8.0.108/runtime'
make[1]: *** [Makefile:549: all-recursive] Error 1
make[1]: Leaving directory '/build/mono-5.8.0.108'
make: *** [Makefile:479: all] Error 2
builder for '/nix/store/5as7c4z3r4h9xjwl96r9jqcbs5fn1yzx-mono-5.8.0.108.drv' failed with exit code 2
cannot build derivation '/nix/store/jh587f41615yqg0zd1k69zvx9r8bdy2j-dotnetbuildhelpers.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/lic42f6n9s8x0r5rj7yay23amckg1664-NUnit.Runners-2.6.4.drv': 2 dependencies couldn't be built
cannot build derivation '/nix/store/3j3ky26cwig40i3v1g1lz2590bnqrnjf-Boogie-unstable-2017-01-03.drv': 3 dependencies couldn't be built
cannot build derivation '/nix/store/vlsy07nhc0m375dh8gcgz32j2bh961x4-Dafny-2.1.0.drv': 3 dependencies couldn't be built
�[31;1merror:�[0m build of '/nix/store/3j3ky26cwig40i3v1g1lz2590bnqrnjf-Boogie-unstable-2017-01-03.drv', '/nix/store/kap02c2ky9qsz5mnd6dd4zgivbgc3rzm-fstar-0.9.6.0.drv', '/nix/store/vlsy07nhc0m375dh8gcgz32j2bh961x4-Dafny-2.1.0.drv' failed

GrahamcOfBorg · 2018-05-25T13:45:57Z

Success on aarch64-linux (full log)

Attempted: z3

Partial log (click to expand)

/nix/store/439yl2qy4lgkfinsk97r72bd5f8qnk66-z3-4.7.1

GrahamcOfBorg · 2018-05-25T13:46:01Z

Success on x86_64-linux (full log)

Attempted: z3

Partial log (click to expand)

/nix/store/52wf44pvqi6x2ws1wcrlzjmr8sjm0na7-z3-4.7.1

GrahamcOfBorg · 2018-05-25T13:46:01Z

Success on x86_64-darwin (full log)

Attempted: z3

Partial log (click to expand)

/nix/store/xsimdipp531qbbyy5j4xj91p4vbv7za1-z3-4.7.1

dtzWill · 2018-05-25T21:56:05Z

I think all the "failures" are due to build timeouts?

update:

boogie build failure pre-existing

Mic92 · 2018-05-25T23:47:28Z

@taktoa regarding broken boogie package.

xeji · 2018-05-30T21:42:19Z

boogie was fixed in #41169

GrahamcOfBorg · 2018-05-30T22:23:06Z

Success on x86_64-linux (full log)

Attempted: z3

Partial log (click to expand)

Z3Py was installed at /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1/lib/python2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1
shrinking /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1/bin/z3
shrinking /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1/lib/libz3.so
strip is /nix/store/92d2ifxcni4n3zx9s8wnkcjlvnx5ajlc-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1/lib  /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1/bin
patching script interpreter paths in /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1
checking for references to /build in /nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1...
/nix/store/79ndy4dbp3b2wvb7whi56nk9r86m35m8-z3-4.7.1

GrahamcOfBorg · 2018-05-30T22:23:31Z

Success on aarch64-linux (full log)

Attempted: z3

Partial log (click to expand)

Z3Py was installed at /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1/lib/python2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1
shrinking /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1/lib/libz3.so
shrinking /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1/bin/z3
strip is /nix/store/8yfik687kfccisxnad42j19lfb7ij9b4-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1/lib  /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1/bin
patching script interpreter paths in /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1
checking for references to /build in /nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1...
/nix/store/nbwnqz3sbh5g2b1xg0fpf63x29agckj5-z3-4.7.1

dtzWill · 2018-05-30T23:05:11Z

@GrahamcOfBorg build boogie souper isabelle haskellPackages.z3

GrahamcOfBorg · 2018-05-30T23:15:17Z

Success on x86_64-linux (full log)

Attempted: boogie, souper, isabelle, haskellPackages.z3

Partial log (click to expand)

checking for references to /build in /nix/store/k3gwky9zayj2y3wvkq1q5lki8r35a3dr-z3-4.3.1...
wrong ELF type
shrinking RPATHs of ELF executables and libraries in /nix/store/y8c849c7qm4lvk0a2g4csxpybfk92yqb-z3-4.3.1-doc
strip is /nix/store/92d2ifxcni4n3zx9s8wnkcjlvnx5ajlc-binutils-2.30/bin/strip
patching script interpreter paths in /nix/store/y8c849c7qm4lvk0a2g4csxpybfk92yqb-z3-4.3.1-doc
checking for references to /build in /nix/store/y8c849c7qm4lvk0a2g4csxpybfk92yqb-z3-4.3.1-doc...
/nix/store/xdl0gcqk2w6hw0a027yvkkaiwyi3pnp4-Boogie-unstable-2018-05-28
/nix/store/0xbavan0b901wf6b3yrszi8038frckjf-souper-unstable-2017-03-23
/nix/store/k8z6p2ppmbhzcizdzlv2j98qw0wr3kvm-isabelle-2017
/nix/store/k3gwky9zayj2y3wvkq1q5lki8r35a3dr-z3-4.3.1

GrahamcOfBorg · 2018-05-30T23:50:28Z

Failure on aarch64-linux (full log)

Attempted: boogie, souper

The following builds were skipped because they don't evaluate on aarch64-linux: isabelle, haskellPackages.z3

Partial log (click to expand)

make[2]: Leaving directory '/build/mono-5.8.0.108/runtime'
make[1]: *** [Makefile:549: all-recursive] Error 1
make[1]: Leaving directory '/build/mono-5.8.0.108'
make: *** [Makefile:479: all] Error 2
builder for '/nix/store/zs0zps5w74vs6abkg0zdg7sqj7hfkywv-mono-5.8.0.108.drv' failed with exit code 2
cannot build derivation '/nix/store/r9gzgfiw41pj5wi5ga4mcky5makxisf4-dotnetbuildhelpers.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/vghxzpcpwidi2mggvi1syjqamsvjc9k1-NUnit-2.6.4.drv': 2 dependencies couldn't be built
cannot build derivation '/nix/store/9jaab31i5zknmavhcinfnqvzvg735clb-NUnit.Runners-2.6.4.drv': 2 dependencies couldn't be built
cannot build derivation '/nix/store/gybpwky1rblmwwxybx93m8k7jramwf9a-Boogie-unstable-2018-05-28.drv': 4 dependencies couldn't be built
�[31;1merror:�[0m build of '/nix/store/gybpwky1rblmwwxybx93m8k7jramwf9a-Boogie-unstable-2018-05-28.drv' failed

GrahamcOfBorg · 2018-05-31T00:41:37Z

Success on x86_64-darwin (full log)

Attempted: z3

Partial log (click to expand)

clang++ -o libz3.dylib -dynamiclib api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_algebraic.o api/api_arith.o api/api_array.o api/api_ast.o api/api_ast_map.o api/api_ast_vector.o api/api_bv.o api/api_commands.o api/api_config_params.o api/api_context.o api/api_datalog.o api/api_datatype.o api/api_fpa.o api/api_goal.o api/api_interp.o api/api_log.o api/api_log_macros.o api/api_model.o api/api_numeral.o api/api_opt.o api/api_params.o api/api_parsers.o api/api_pb.o api/api_polynomial.o api/api_qe.o api/api_quant.o api/api_rcf.o api/api_seq.o api/api_solver.o api/api_stats.o api/api_tactic.o api/z3_replayer.o opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a ast/proofs/proofs.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a
cp libz3.dylib python
Z3Py was installed at /nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1/lib/python2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
post-installation fixup
strip is /nix/store/r5mcn9vqq80v5pfqp45d7290cis7dwp4-cctools-binutils-darwin/bin/strip
stripping (with command strip and flags -S) in /nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1/lib  /nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1/bin
patching script interpreter paths in /nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1
/nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1/lib/libz3.dylib: fixing dylib
/nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1/lib/python2.7/site-packages/z3/lib/libz3.dylib: fixing dylib
/nix/store/4wrf00zq59r9wb99cwb71z9znq4isqn1-z3-4.7.1

GrahamcOfBorg · 2018-05-31T01:36:24Z

Failure on x86_64-darwin (full log)

Attempted: boogie, haskellPackages.z3

The following builds were skipped because they don't evaluate on x86_64-darwin: souper, isabelle

Partial log (click to expand)

CSC     [xbuild_14] Microsoft.Build.Framework.dll
CSC     [xbuild_14] Microsoft.Build.Utilities.Core.dll
Microsoft.Build.Utilities/TaskLoggingHelper.cs(39,16): warning CS0169: The field 'TaskLoggingHelper.buildEngine' is never used
CSC     [xbuild_14] Microsoft.Build.Engine.dll
building of '/nix/store/s8hfqbljvvcygkig5lw2h3ndxn0va5kv-mono-5.8.0.108.drv' timed out after 1800 seconds
cannot build derivation '/nix/store/krhqq5qdi5m7hlza5a2ym9ykyiv4rkgy-dotnetbuildhelpers.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/315grwby96f778a3bgxpjxailw4iv98f-NUnit-2.6.4.drv': 2 dependencies couldn't be built
cannot build derivation '/nix/store/dw187dm5vgr43zpzc149bvrbzr53abr1-NUnit.Runners-2.6.4.drv': 2 dependencies couldn't be built
cannot build derivation '/nix/store/x8ydnnzsyc3psd93bgnxcwaga5dr1n75-Boogie-unstable-2018-05-28.drv': 4 dependencies couldn't be built
error: build of '/nix/store/x8ydnnzsyc3psd93bgnxcwaga5dr1n75-Boogie-unstable-2018-05-28.drv' failed

dtzWill · 2018-05-31T01:50:17Z

@build haskellPackages.z3 haskellPackages.linearEqSolver haskellPackages.sbv haskellPackages.ez3 cryptol

dtzWill · 2018-06-06T15:43:03Z

Whoops re:summoning ofborg. Anyway, LGTM.

dtzWill requested a review from thoughtpolice May 25, 2018 02:23

GrahamcOfBorg added 10.rebuild-darwin: 11-100 10.rebuild-linux: 11-100 labels May 25, 2018

dtzWill force-pushed the update/z3-4.7.1 branch from 33d72cd to 24d50b4 Compare May 25, 2018 13:33

z3: 4.6.0 -> 4.7.1

edbebe7

dtzWill force-pushed the update/z3-4.7.1 branch from 24d50b4 to edbebe7 Compare May 30, 2018 21:54

dtzWill merged commit 19b4ec9 into NixOS:master Jun 6, 2018

dtzWill deleted the update/z3-4.7.1 branch June 6, 2018 15:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

z3: 4.6.0 -> 4.7.1 #41068

z3: 4.6.0 -> 4.7.1 #41068

dtzWill commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

Mic92 commented May 25, 2018

Mic92 commented May 25, 2018

Mic92 commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

dtzWill commented May 25, 2018 •

edited

Loading

Mic92 commented May 25, 2018

xeji commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

dtzWill commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

GrahamcOfBorg commented May 31, 2018

GrahamcOfBorg commented May 31, 2018

dtzWill commented May 31, 2018

dtzWill commented Jun 6, 2018

z3: 4.6.0 -> 4.7.1 #41068

z3: 4.6.0 -> 4.7.1 #41068

Conversation

dtzWill commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

Mic92 commented May 25, 2018

Mic92 commented May 25, 2018

Mic92 commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

GrahamcOfBorg commented May 25, 2018

dtzWill commented May 25, 2018 • edited Loading

Mic92 commented May 25, 2018

xeji commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

dtzWill commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

GrahamcOfBorg commented May 30, 2018

GrahamcOfBorg commented May 31, 2018

GrahamcOfBorg commented May 31, 2018

dtzWill commented May 31, 2018

dtzWill commented Jun 6, 2018

dtzWill commented May 25, 2018 •

edited

Loading