Skip to content

Add Z3 4.15.1 #28015

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 13 commits into from
Jun 19, 2025
Merged

Add Z3 4.15.1 #28015

merged 13 commits into from
Jun 19, 2025

Conversation

wintersteiger
Copy link
Contributor

No description provided.

@wintersteiger
Copy link
Contributor Author

The Windows CI seems to suffer from some basic setup problems:

Run D:\opam\bin\opam --version
D:\opam\bin\opam: C:\a\_temp\19a2dd70-5a50-4a2d-a927-725b5474702d.ps1:2
Line |
   2 |  D:\opam\bin\opam --version
     |  ~~~~~~~~~~~~~~~~
     | The term 'D:\opam\bin\opam' is not recognized as a name of a cmdlet, function, script file, or executable
     | program. Check the spelling of the name, or if a path was included, verify that the path is correct and try
     | again.
Error: Process completed with exit code 1.

In previous Z3 releases we always ignored the Windows CI because it used the wrong compiler. I believe I now have an idea why: conf-python-3 uses the Windows Python (default, from app store), i.e. it reports nt as the os.name, while the Cygwin Python would return posix.

@wintersteiger wintersteiger marked this pull request as draft June 11, 2025 16:50
@wintersteiger wintersteiger marked this pull request as ready for review June 11, 2025 19:53
@wintersteiger
Copy link
Contributor Author

This one's ready for review/merge. The CI problems are expected/false positives.

@shonfeder
Copy link
Contributor

Thank you for publishing this important update and for taking care of reviewing and fixing the CI! Indeed, the remaining errors are not relevant.

@shonfeder shonfeder merged commit efba6c4 into ocaml:master Jun 19, 2025
0 of 2 checks passed
@arbipher
Copy link
Contributor

Hi, I am working on building ocaml-z3 from CMake. It's not fully done yet, but both my forked z3 and the opam packages work well on CI (currently GitHub Actions). I put some updates Z3Prover/z3#7684.

I saw Windows CI discussed here. May I ask for more background and status? I also don't understand why llvm is put in the building path, which looks a fragile dependency,

@wintersteiger
Copy link
Contributor Author

The Opam CI runs on many different platforms, see for example one of the test runs for this PR (e.g https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/eb1839f6536e00144ff383f35c0878f9cb0c30a2) and that does indeed include Windows.

The current Opam Windows CI is either misconfigured or the conf-python package is broken (depending on how you want to look at it), It uses the first Python it finds, which happens to be the Windows-Python, when it really wants a Cygwin-Python and the Z3 scripts complain that MSVC is not installed.

The LLVM dependency only exists for the homebrew setup, which was recently add to the Opam CI. Depending on how you want to look at it, it's also misconfigured or the conf-c++ package is broken as it does not make sure there is a C++ compiler in the path. So, for now it gets a compiler from the homebrew eco-system and I picked LLVM for no particular reason.

@wintersteiger wintersteiger deleted the wintersteiger/z3.4.15.1 branch June 19, 2025 13:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants