Add Z3 4.12.3

[wintersteiger]

This adds the latest Z3 release.

[arbipher]

@kit-ty-kate has pinpointed the error message is raised at this mk_util.py/compileall.compile_dir (doc for py_compile).

I re-do the experiment on my macOS 13.5 with ocaml 5.1.1-rc and I can confirm the same problem on recent versions z3 with this error message in the log

/usr/local/Cellar/python@3.11/3.11.6_1/Frameworks/Python.framework/Versions/3.11/Resources/Python.app/Contents/MacOS/Python: can't open file '/Users/ex/.opam/5.1.1~rc1/.opam-switch/build/z3.4.12.3/scripts/mk_make.py': [Errno 2] No such file or directory

(edit: this error message may be not related. I am still debugging)
(edit2: I cannot make it re-appear on my mac)

The only difference between 4.12.2-1 and 4.12.3 is the checksum and the gcc-fix (which I think should also be in this PR but no related to the current problem). I can still compile z3 with ocaml 5.1.1 so that I think the problem is related to the handling of python in ocaml 5.1.1-rc.

[arbipher]

At this moment, I am not clear about whether it's related to #24742 .

[wintersteiger]

Thanks for taking a look at this!

Just yesterday, we have seen the same problem as in the CI runs on the previous version of Z3 (4.12.2-1), on a freshly upgraded MacOS Sonoma, however I wasn't able to reproduce the problem myself yet (on Sonoma or elsewhere).

This is not about files not being found, but about permissions to the Python compilation cache. During mk_make.py, the build tries to pre-compile the Z3 Python API files (*.py -> *.pyc, etc), by calling the Python compiler (compile_dir), but for some reason the compiler doesn't have access to the cache directory for the precompiled files. I suspect this is highly dependent on the way that Python is installed on the system, because the cache directories end up in different places depending on how it is installed (that's also why I couldn't reproduce it yet.)

Is there a way for me to get access to the macos-homebrew-ocaml-5.1 Docker image, so that I can reproduce the CI run locally?

[wintersteiger]

Oh, the gcc-fix patch isn't required anymore as that change has been merged into Z3 itself since the previous release.

[arbipher]

@wintersteiger
I agree with your observations on Python permission. I need some time to investigate it.

Thanks for the explanation for the gcc-fix patch.

[arbipher]

Is there a way for me to get access to the macos-homebrew-ocaml-5.1 Docker image, so that I can reproduce the CI run locally?

Here is the recap from the chat with @kit-ty-kate .

The macos-homebrew-ocaml-5.1 is not a docker image. The macos pipeline is defined in ocurrent/macos-infra and used by ocurrent/opam-repo-ci. It may be possible to call custom dune rules with ocurrent/ocaml-ci as our method to pinpoint some situations under the same macos environment.

I need some time to investigate it (again).

p.s. I am more inclined to think it's related to macOS security policy in the CI images rather than any ocaml/opam/z3 problem but still need experiments to confirm it. I can install the PR-ed version of z3 with my local 5.1.1-rc without problems.

[wintersteiger]

That's a very good point - it may indeed be some new security policy.

[mseri]

What is the state of this? Looks like is just the CI being stricter to me, but do you think you should look into it more carefully to ensure compatibility with mac before we merge?

[wintersteiger]

I'm still trying to reproduce the failure, unsuccessfully so far. It only seems to happen on newer MacOS Sonoma's, on which installation of the current Z3 package (4.12.2-1) fails also. It seems to be some sort of system-controlled flavour of Python that triggers it because of more restrictive user permissions or security policies.

[arbipher]

I haven't done (not a good time to) embark on ocurrent/macos-infra yet. I will do but I am afraid I block any merging here if they work for most of the time. I cannot reproduce it myself.

ocurrent/macos-infra has mentioned SIP. Another maybe related issue is mac's legacy support for scripting language.

[wintersteiger]

I've added a patch to make the Python bytecode compilation optional. Sorry for abusing the CI, but I just can't reproduce the problem anywhere else.

[wintersteiger]

Also, I finally managed to reproduce it. It's the Python 3.9 that comes with XCode that creates a cache in ~/Library/Caches and the brew-installed version does not. It's possible that the MacOS CI setup installs a good version, but then accidentally uses the other one because of the order of directories in the PATH.

[arbipher]

Great work for detecting this (and also for the fix)!

[wintersteiger]

Two nuscr package builds failed during the CI run. I have no idea what those packages are and what they do, but I think it has nothing to do with Z3?

[arbipher]

Thank you for the two z3 pushes. They look good to me.
I also don't think the nurse's failure is related to z3. Their failure is due to mismatch of their cram-tests, which doesn't look related here.

[mseri]

Don't worry about that. It is not related and seems only a innocuous cram test output change

[mseri]

Thanks