z3: update to 4.13.0

[barracuda156]

Description

Update

Type(s)

• bugfix
• enhancement
• security fix

Tested on

macOS 10.6
Xcode 3.2

Verification

Have you

• followed our Commit Message Guidelines?
• squashed and minimized your commits?
• checked that there aren't other open pull requests for the same change?
• referenced existing tickets on Trac with full URL in commit message?
• checked your Portfile with port lint --nitpick?
• tried existing tests with sudo port test?
• tried a full install with sudo port -vst install?
• tested basic functionality of all binary files?
• checked that the Portfile's most important variants haven't been broken?

[macportsbot]

Notifying maintainers:
@landonf for port z3.

[ryandesign]

z3 is failing at the test phase with:

DEBUG: system -W /opt/local/var/macports/build/_Users_runner_work_macports-ports_macports-ports_ports_math_z3/z3/work/build: ./test-z3 /a
sh: ./test-z3: No such file or directory
Command failed: ./test-z3 /a
Exit code: 127

I thought mpbb was only running MacPorts built-in tests, not the ones defined in the Portfile. But I see this is coming from a post-test block in the Portfile. @jmroot, is this a bug in base or mpbb, or something that needs to be changed in the way the Portfile runs its tests?

z3-fstar is failing due to:

ModuleNotFoundError: No module named 'distutils'

[barracuda156]

@ryandesign I just installed locally z3-fstar on Sonoma, so that one is perhaps a mere dependency missing after something again changed in Python build systems.

svacchanda@43-78 ~ % port -v installed z3-fstar
The following ports are currently installed:
  z3-fstar @4.8.5_5+lto+pgo+polly+polly_late+polly_vector (active) requested_variants='' platform='darwin 23' archs='arm64' date='2024-04-13T14:54:23+0800'

[jmroot]

I thought mpbb was only running MacPorts built-in tests, not the ones defined in the Portfile. But I see this is coming from a post-test block in the Portfile. @jmroot, is this a bug in base or mpbb, or something that needs to be changed in the way the Portfile runs its tests?

Hm, yeah, post-test blocks get executed whether or not test.run is true. I guess it's debatable whose problem this is.

[ryandesign]

I just installed locally z3-fstar on Sonoma, so that one is perhaps a mere dependency missing after something again changed in Python build systems.

I assume you received the binary which we built January 11, 2024, back when the port was building with python311. The port's python version was changed to python312 in 4c09b10 on January 24, 2024, without apparently verifying that it could still build.

distutils was a deprecated part of python until it was removed in python312. To get that functionality back you would add a dependency on py312-setuptools.

[ryandesign]

Hm, yeah, post-test blocks get executed whether or not test.run is true. I guess it's debatable whose problem this is.

On the basis that there was nothing wrong with the way the port was running its tests before base gained the ability to run built-in tests, I suggest that it should be base's problem to fix.

If it were the port's problem, though, how would it do it? Obviously in this specific case it could check in the post-test block whether test-z3 exists before running it, but is there a general way that a portfile can know whether the full tests or just the built-in tests are being run?

[jmroot]

If it were the port's problem, though, how would it do it? Obviously in this specific case it could check in the post-test block whether test-z3 exists before running it, but is there a general way that a portfile can know whether the full tests or just the built-in tests are being run?

Check whether test.run is true.

[ryandesign]

Check whether test.run is true.

So the port sets test.run yes but MacPorts changes it? Weird.

In what situation would it make sense for MacPorts to run a port's pre-test or post-test blocks if its tests aren't going to be run?

There are currently 105 ports with pre-test and/or post-test blocks. Shall we add this check to all of them?

[ryandesign]

I consider this a bug in the new built-in tests and have filed https://trac.macports.org/ticket/69866.

[barracuda156]

@ryandesign Thank you!

Hopefully this gets sorted soon and we are not stuck with updates indefinitely.

[pmetzger]

How do we get this moving again?

[barracuda156]

How do we get this moving again?

Did I miss something or it is still a bug in CI? I can’t do anything about that, obviously.

If something should be done about z3 itself, that is doable.

[jmroot]

I'm pretty sure the z3-fstar build failure isn't a CI bug.

[barracuda156]

@jmroot I don’t touch that subport here, somehow it worked before?

[pmetzger]

None the less, it would be useful to figure out why it is failing. There's sadly an element of "if you touch it, you should see if you can fix it" about our maintenance philosophy, but that's not actually bad.

[barracuda156]

@pmetzger I suggest someone knowing Python build system to deal with this:

  Traceback (most recent call last):
    File "/opt/local/var/macports/build/_Users_runner_work_macports-ports_macports-ports_ports_math_z3/z3-fstar/work/z3-Z3-4.8.5/scripts/update_api.py", line 18, in <module>
      import mk_util
    File "/opt/local/var/macports/build/_Users_runner_work_macports-ports_macports-ports_ports_math_z3/z3-fstar/work/z3-Z3-4.8.5/scripts/mk_util.py", line 18, in <module>
      import distutils.sysconfig
  ModuleNotFoundError: No module named 'distutils'
  FAILED: src/api/api_commands.cpp src/api/api_log_macros.cpp src/api/api_log_macros.h /opt/local/var/macports/build/_Users_runner_work_macports-ports_macports-ports_ports_math_z3/z3-fstar/work/build/src/api/api_commands.cpp /opt/local/var/macports/build/_Users_runner_work_macports-ports_macports-ports_ports_math_z3/z3-fstar/work/build/src/api/api_log_macros.cpp /opt/local/var/macports/build/_Users_runner_work_macports-ports_macports-ports_ports_math_z3/z3-fstar/work/build/src/api/api_log_macros.h 

It has probably been broken by a global switch to a pep517 without testing if it actually works for all ports.

[jmroot]

It has probably been broken by a global switch to a pep517 without testing if it actually works for all ports.

No, it would have been broken by 4c09b10.

[barracuda156]

@jmroot Fair enough, but it cannot be broken by this PR, since -star subport is not changed.

[jmroot]

I'm not seeking to assign blame here, but you seem to want CI to pass, and fixing that build failure is how that will happen.

[barracuda156]

@jmroot Maybe you could suggest something, since you know Python build system?

[jmroot]

https://docs.python.org/3/whatsnew/3.12.html

Remove the distutils package. See the migration guide for advice replacing the APIs it provided. The third-party Setuptools package continues to provide distutils, if you still require it in Python 3.12 and beyond.

I don't know if the dependency is needed at runtime or only at build time.

[jmroot]

As per lint:
Warning: Dependency port:python312 specified multiple times in depends_build
That's because most of this has already been done around line 93.