z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 #327052

numinit · 2024-07-14T07:59:20Z

Description of changes

nixpkgs z3 default is now 4.13 instead of 4.8.
Fixing breakage due to setuptools removal in [python-updates] major updates, python 3.12 as default - 2024-06-19 #320924 for z3 4.8
Adding more z3 versions and updating existing ones
Making the checkPhase go faster

Resolves #326120.

Things done

Add a 👍 reaction to pull requests you find important.

pkgs/applications/science/logic/z3/default.nix

numinit · 2024-10-14T02:29:57Z

Rebased.

FliegendeWurst · 2024-10-16T21:18:07Z

ofborg complains about a test failure on Mac:

       > xxx
       > (or (and true (not (not true))) (and true (not (not false)))) true
       > /nix/store/qkjcgnzm56frvkvsm4q66bf75bq9z6v2-stdenv-darwin/setup: line 1720: 71274 Segmentation fault: 11  ./test-z3 -a
       For full logs, run 'nix log /nix/store/yhglasr16smlyilskm2wy1s4n62bkqz6-z3-4.8.17.drv'.
error: building of '/nix/store/5jynspwpzb77mmgsl93amdrjj5s6m7jf-z3-4.13.3.drv^out' from .drv file timed out after 3600 seconds
error: build of '/nix/store/5jynspwpzb77mmgsl93amdrjj5s6m7jf-z3-4.13.3.drv', '/nix/store/yhglasr16smlyilskm2wy1s4n62bkqz6-z3-4.8.17.drv' failed

numinit · 2024-10-16T21:25:31Z

Weird. Technically the only way I affected that build was adding the -j $NIX_BUILD_CORES to checkPhase...

numinit · 2024-10-16T21:36:24Z

I'll try another approach, probably just going to disable the parallel test build on MacOS.

numinit · 2024-10-17T03:06:04Z

Wait, that doesn't seem like the problem:

/nix/store/qkjcgnzm56frvkvsm4q66bf75bq9z6v2-stdenv-darwin/setup: line 1720: 71274 Segmentation fault: 11 ./test-z3 -a

The actual test runner isn't even run in parallel!

numinit · 2024-10-17T03:22:49Z

8e5e9e9

Presumably this problem is only for legacy versions. One would hope. 🙃

FliegendeWurst · 2024-10-17T06:43:59Z

Well it still fails after 3 retries. It is odd that it still passes on Linux.

numinit · 2024-10-17T07:10:08Z

Let's find out whether it's the ordering of test source files that's causing an only-on-Darwin segfault...

numinit · 2024-10-17T07:26:40Z

Possible places something was fixed:

Z3Prover/z3#6116
Z3Prover/z3#6535

numinit · 2024-10-17T17:09:18Z

Now I wonder if the previous success was spurious...

I also maintain KLEE and STP, and use z3.

Original commit message by Reno Dakota (https://github.com/paparodeo), rebased against latest z3 changes: z3 contains a bunch of typos in never used functions. The update to clang-19 now reports the typos -- wrong member function / variable names. There is an upstream patch which fixes some of these: Z3Prover/z3@2ce89e5 And the others we patch or remove as the upstream code has since been modified.

numinit · 2025-01-12T01:53:30Z

Resolved issues with Z3 Haskell libraries.

numinit · 2025-01-12T03:49:08Z

`nixpkgs-review` result

Generated using nixpkgs-review.

Command: nixpkgs-review

`x86_64-linux`

⏩ 16 packages marked as broken and skipped:

python312Packages.angr
python312Packages.angr.dist
python312Packages.angrcli
python312Packages.angrcli.dist
python312Packages.angrop
python312Packages.angrop.dist
python312Packages.cynthion
python312Packages.cynthion.dist
python312Packages.luna-soc
python312Packages.luna-soc.dist
python312Packages.luna-usb
python312Packages.luna-usb.dist
python313Packages.luna-soc
python313Packages.luna-soc.dist
python313Packages.luna-usb
python313Packages.luna-usb.dist

⏩ 1 package blacklisted:

nixos-install-tools

❌ 4 packages failed to build:

isabelle
isabelle-components.isabelle-linter
tlaps
ugarit

✅ 90 packages built:

acl2
alive2
circt
circt.dev
circt.lib
cynthion
cynthion.dist
dafny
foundry
fstar
glasgow
glasgow.dist
hal-hardware-analyzer
iprover
klee
libbap
ocamlPackages.z3
pony-corral
ponyc
python312Packages.amaranth
python312Packages.amaranth-boards
python312Packages.amaranth-boards.dist
python312Packages.amaranth-soc
python312Packages.amaranth-soc.dist
python312Packages.amaranth.dist
python312Packages.bap
python312Packages.bap.dist
python312Packages.claripy
python312Packages.claripy.dist
python312Packages.deal
python312Packages.deal-solver
python312Packages.deal-solver.dist
python312Packages.deal.dist
python312Packages.icontract
python312Packages.icontract.dist
python312Packages.miasm
python312Packages.miasm.dist
python312Packages.model-checker
python312Packages.model-checker.dist
python312Packages.pylddwrap
python312Packages.pylddwrap.dist
python312Packages.z3-solver (python312Packages.z3-solver.dev ,python312Packages.z3-solver.lib ,python312Packages.z3-solver.python)
python313Packages.amaranth
python313Packages.amaranth-boards
python313Packages.amaranth-boards.dist
python313Packages.amaranth-soc
python313Packages.amaranth-soc.dist
python313Packages.amaranth.dist
python313Packages.bap
python313Packages.bap.dist
python313Packages.claripy
python313Packages.claripy.dist
python313Packages.deal
python313Packages.deal-solver
python313Packages.deal-solver.dist
python313Packages.deal.dist
python313Packages.icontract
python313Packages.icontract.dist
python313Packages.model-checker
python313Packages.model-checker.dist
python313Packages.pylddwrap
python313Packages.pylddwrap.dist
python313Packages.z3-solver (python313Packages.z3-solver.dev ,python313Packages.z3-solver.lib ,python313Packages.z3-solver.python)
sail-riscv-rv32
sail-riscv-rv64
sby
solc
symcc
vampire
z3
z3-tptp
z3.dev
z3.lib
z3.python
z3_4_11
z3_4_11.dev
z3_4_11.lib
z3_4_11.python
z3_4_12
z3_4_12.dev
z3_4_12.lib
z3_4_12.python
z3_4_8
z3_4_8.dev
z3_4_8.lib
z3_4_8.python
z3_4_8_5
z3_4_8_5.dev
z3_4_8_5.lib
z3_4_8_5.python

sternenseemann

Haskell stuff LGTM. Skimmed the rest.

Sorry for the endless back and forth!

numinit · 2025-01-12T22:43:48Z

No problem!

numinit · 2025-01-13T02:14:41Z

Failures are unrelated to z3:

isabelle:

error: builder for '/nix/store/6j0067n8yqsi7xzk113rr0xi8lmpfhmc-polyml-for-isabelle-2024.drv' failed with exit code 2;
       last 25 log lines:
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o sharedata.lo sharedata.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c sharedata.cpp -o sharedata.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o sighandler.lo sighandler.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c sighandler.cpp -o sighandler.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o statistics.lo statistics.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c statistics.cpp -o statistics.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o timing.lo timing.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c timing.cpp -o timing.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o xwindows.lo xwindows.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c xwindows.cpp -o xwindows.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o x86_dep.lo x86_dep.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c x86_dep.cpp -o x86_dep.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CC   --mode=compile gcc -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"     -c -o x86assembly_gas64.lo x86assembly_gas64.S
       > libtool: compile:  gcc -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -c x86assembly_gas64.S -o x86assembly_gas64.o
       > /nix/store/5mh7kaj2fyv8mk4sfq1brwxgc02884wi-bash-5.2p37/bin/bash ../libtool  --tag=CXX   --mode=compile g++ -DHAVE_CONFIG_H -I. -I..  -O3   -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\"    -O3 -c -o elfexport.lo elfexport.cpp
       > libtool: compile:  g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Wall -DMODULEDIR=\"/nix/store/8110nnykrk36ik8zz7h00q3bg133gphx-polyml-for-isabelle-2024/lib/polyml/modules\" -O3 -c elfexport.cpp -o elfexport.o
       > In file included from elfexport.cpp:98:
       > /nix/store/kj8hbqx4ds9qm9mq7hyikxyfwwg13kzj-glibc-2.40-36-dev/include/asm/elf.h:14:15: error: expected constructor, destructor, or type conversion before '(' token
       >    14 | _Static_assert(sizeof(struct x86_xfeat_component) % 4 == 0, "x86_xfeat_component is not aligned");
       >       |               ^
       > make[2]: *** [Makefile:766: elfexport.lo] Error 1
       > make[2]: Leaving directory '/build/source/libpolyml'
       > make[1]: *** [Makefile:710: all-recursive] Error 1
       > make[1]: Leaving directory '/build/source'
       > make: *** [Makefile:469: all] Error 2

tlaps is the same thing.

ugarit:

error: builder for '/nix/store/sqazfyxzbm7js921m63zpg5lppbbq7j4-chicken-posix-extras-0.1.6.drv' failed with exit code 1;
       last 25 log lines:
       >       |                                                        ^
       > posix-extras.c:833:8: note: in expansion of macro 'C_major'
       >   833 | av2[1]=C_major(t2);
       >       |        ^~~~~~~
       > posix-extras.c: In function 'f_724':
       > posix-extras.c:44:41: error: implicit declaration of function 'minor' [8;;https://gcc.gnu.org/onlinedocs/gcc-14.2.0/gcc/Warning-Options.html#index-Wimplicit-function-declaration-Wimplicit-function-declaration8;;]
       >    44 | #define C_minor(d) C_fix((unsigned int) minor(C_num_to_unsigned_long(d)))
       >       |                                         ^~~~~
       > /nix/store/x421qn2s409qsl084j8n73khnsa60g8m-chicken-4.13.0/include/chicken/chicken.h:1043:56: note: in definition of macro 'C_fix'
       >  1043 | #define C_fix(n)                   ((C_word)((C_uword)(n) << C_FIXNUM_SHIFT) | C_FIXNUM_BIT)
       >       |                                                        ^
       > posix-extras.c:1614:8: note: in expansion of macro 'C_minor'
       >  1614 | av2[1]=C_minor(t2);
       >       |        ^~~~~~~
       >
       > Error: shell command terminated with non-zero exit status 256: 'gcc' 'posix-extras.c' -o 'posix-extras.o' -c  -fno-strict-aliasing -fwrapv -DHAVE_CHICKEN_CONFIG_H -DC_ENABLE_PTABLES -Os -fomit-frame-pointer -fPIC -DPIC -DC_SHARED -I/nix/store/x421qn2s409qsl084j8n73khnsa60g8m-chicken-4.13.0/include/chicken
       >
       > Error: shell command failed with nonzero exit status 256:
       >
       >   '/nix/store/x421qn2s409qsl084j8n73khnsa60g8m-chicken-4.13.0/bin/csc' -feature compiling-extension -setup-mode    -s -O2 -d1 -inline -local posix-extras.scm -J
       >
       >
       > Error: shell command terminated with nonzero exit code
       > 17920
       > "'/nix/store/x421qn2s409qsl084j8n73khnsa60g8m-chicken-4.13.0/bin/csi' -bnq -setu...

Created #373346 and #373347.

numinit · 2025-01-13T20:29:18Z

I think this should be ready to merge and backport.

sternenseemann · 2025-01-14T11:19:23Z

This would need to be backported without the default version upgrade (4.8.17 -> 4.13.4) since it's ostensibly a breaking change.

numinit · 2025-01-15T01:02:26Z

I think the only real changes have been soundness fixes and compiler compatibility. We could do a manual backport that doesn't switch the default, though. Someone is bound to be depending on it.

sternenseemann · 2025-01-15T11:52:57Z

@numinit But packages in nixpkgs were broken by the update, right? Thus we should assume that it'd also affect downstream packages.

numinit · 2025-01-15T17:36:43Z

Yes, it was all due to the Z3_TRUE/Z3_FALSE header change, though (and that was just the Haskell ones). I do agree about keeping the default on 4.8 in 24.11 in case there are other things even though it ended up mostly being fine otherwise.

nixpkgs-ci · 2025-01-17T01:24:43Z

Backport failed for release-24.11, because it was unable to cherry-pick the commit(s).

Please cherry-pick the changes locally and resolve any conflicts.

git fetch origin release-24.11
git worktree add -d .worktree/backport-327052-to-release-24.11 origin/release-24.11
cd .worktree/backport-327052-to-release-24.11
git switch --create backport-327052-to-release-24.11
git cherry-pick -x 2cb20cbfc26056e46a86bc72742c4d63332a7834 5a15eeca82b9c33772380699b4d4e50203783bde ef1388f5283f7ed759d8b2859ca24f2d56c2c759 fc7bc1d7ccde12e4e89b82eac63137f33100c59c 2ad2eedce2138d3cbff95c1db32d5881221304ad 9d557ee2d49a44e134110b333ddf6088f3b7b933 3af07aa4d35df5029509c353220b6801867c882d df9943568857ce91906c76a17c5d7d440376d1ad c556717c444259c8305c182ea6f93ea7b9251dd0

emilytrau · 2025-01-17T01:25:30Z

Thanks for the great work!

numinit requested review from thoughtpolice and ttuegel July 14, 2024 08:04

ofborg bot added 11.by: package-maintainer This PR was created by the maintainer of the package it changes 10.rebuild-darwin: 1-10 10.rebuild-linux: 1-10 labels Jul 14, 2024

numinit added the 0.kind: build failure A package fails to build label Jul 14, 2024

numinit commented Jul 15, 2024

View reviewed changes

pkgs/applications/science/logic/z3/default.nix Outdated Show resolved Hide resolved

numinit force-pushed the z3-fix-4.8.5 branch from c8909d8 to ddf8e22 Compare July 19, 2024 09:01

ofborg bot added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux and removed 10.rebuild-darwin: 1-10 10.rebuild-linux: 1-10 labels Jul 19, 2024

numinit force-pushed the z3-fix-4.8.5 branch from ddf8e22 to f27da22 Compare October 14, 2024 02:29

numinit changed the title ~~z3: fix 4.8.5 compile on Python 3.12~~ z3: fix 4.8.5 compile on Python 3.12; z3_4_12: 4.12.5 -> 4.12.6; z3_4_13: init at 4.13.3 Oct 14, 2024

numinit force-pushed the z3-fix-4.8.5 branch from 8e5e9e9 to c197e1c Compare October 17, 2024 07:09

numinit added 8 commits January 11, 2025 17:43

z3: add numinit as maintainer

5a15eec

I also maintain KLEE and STP, and use z3.

z3_4_12: 4.12.5 -> 4.12.6

ef1388f

z3: 4.8.5 -> 4.13.4

fc7bc1d

z3: run through nixfmt-rfc-style

2ad2eed

z3: add release-notes

9d557ee

haskellPackages.{hz3,z3}: add compile flags for newer Z3 versions

3af07aa

z3: add installCheckPhase

c556717

numinit force-pushed the z3-fix-4.8.5 branch from 425fb9e to c556717 Compare January 12, 2025 01:49

numinit requested review from sternenseemann, RossComputerGuy and wegank January 12, 2025 01:56

sternenseemann approved these changes Jan 12, 2025

View reviewed changes

wegank added 12.approved-by: package-maintainer This PR was reviewed and approved by a maintainer listed in the package 12.approvals: 3+ This PR was reviewed and approved by three or more reputable people labels Jan 14, 2025

emilytrau merged commit bdc45c6 into NixOS:master Jan 17, 2025
28 of 30 checks passed

This was referenced Jan 18, 2025

z3: move relnotes to 25.05 #374872

Merged

[Backport release-24.11] z3_4_12: 4.12.5 -> 4.12.6; z3_4_13: init at 4.13.4; fix Z3 builds #374875

Open

Upgrade F* to use Z3 4.13.3 FStarLang/FStar#3631

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 #327052

z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 #327052

numinit commented Jul 14, 2024 •

edited

Loading

numinit commented Oct 14, 2024

FliegendeWurst commented Oct 16, 2024

numinit commented Oct 16, 2024

numinit commented Oct 16, 2024

numinit commented Oct 17, 2024

numinit commented Oct 17, 2024

FliegendeWurst commented Oct 17, 2024

numinit commented Oct 17, 2024

numinit commented Oct 17, 2024

numinit commented Oct 17, 2024

numinit commented Jan 12, 2025

numinit commented Jan 12, 2025

sternenseemann left a comment

numinit commented Jan 12, 2025

numinit commented Jan 13, 2025 •

edited

Loading

numinit commented Jan 13, 2025

sternenseemann commented Jan 14, 2025

numinit commented Jan 15, 2025 •

edited

Loading

sternenseemann commented Jan 15, 2025

numinit commented Jan 15, 2025 •

edited

Loading

nixpkgs-ci bot commented Jan 17, 2025

emilytrau commented Jan 17, 2025

z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 #327052

z3: 4.8.17 -> 4.13.4; z3_4_12: 4.12.5 -> 4.12.6 #327052

Conversation

numinit commented Jul 14, 2024 • edited Loading

Description of changes

Things done

numinit commented Oct 14, 2024

FliegendeWurst commented Oct 16, 2024

numinit commented Oct 16, 2024

numinit commented Oct 16, 2024

numinit commented Oct 17, 2024

numinit commented Oct 17, 2024

FliegendeWurst commented Oct 17, 2024

numinit commented Oct 17, 2024

numinit commented Oct 17, 2024

numinit commented Oct 17, 2024

numinit commented Jan 12, 2025

numinit commented Jan 12, 2025

nixpkgs-review result

x86_64-linux

sternenseemann left a comment

Choose a reason for hiding this comment

numinit commented Jan 12, 2025

numinit commented Jan 13, 2025 • edited Loading

numinit commented Jan 13, 2025

sternenseemann commented Jan 14, 2025

numinit commented Jan 15, 2025 • edited Loading

sternenseemann commented Jan 15, 2025

numinit commented Jan 15, 2025 • edited Loading

nixpkgs-ci bot commented Jan 17, 2025

emilytrau commented Jan 17, 2025

numinit commented Jul 14, 2024 •

edited

Loading

`nixpkgs-review` result

`x86_64-linux`

numinit commented Jan 13, 2025 •

edited

Loading

numinit commented Jan 15, 2025 •

edited

Loading

numinit commented Jan 15, 2025 •

edited

Loading