z3 @4.13.4: error: Error in reading profile .../z3.profdata: No such file or directory

[lpgaff (Liam Gaffney)]

z3 fails at the configure stage when cmake is testing the compiler. The test build files do not exist and then the configure exits with an error. See log file attached.

[lpgaff (Liam Gaffney)]

verbose output from the fresh z3 build

[lpgaff (Liam Gaffney)]

main log file from fresh z3 build

[ryandesign (Ryan Carsten Schmidt)]

Did cmake leave a log file of some kind somewhere in the work directory? If so please attach that as well.

Is the clang-19 port installed? Does the clang program it installed work?

[lpgaff (Liam Gaffney)]

Attached is the cmake cache file. There are no files in the CMakeScratch directory where it is attempting to do the test compilation (as in the log file):

lpgaff@nslap11 build % pwd
/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_macports_release_tarballs_ports_math_z3/z3/work/build
lpgaff@nslap11 build % ls -lhrt CMakeFiles/CMakeScratch 
total 0
lpgaff@nslap11 build % ls -l ../z3-z3-4.13.4 
total 608
-rw-r--r--   1 macports  wheel   26056  7 Mar 16:11 CMakeLists.txt
-rw-r--r--   1 macports  wheel   25930 16 Dec 11:00 CMakeLists.txt.orig
-rw-r--r--   1 macports  wheel    1096 16 Dec 11:00 LICENSE.txt
-rw-r--r--   1 macports  wheel   19640 16 Dec 11:00 README-CMake.md
-rw-r--r--   1 macports  wheel    9028 16 Dec 11:00 README.md
-rw-r--r--   1 macports  wheel   68011 16 Dec 11:00 RELEASE_NOTES.md
-rw-r--r--   1 macports  wheel   10407 16 Dec 11:00 azure-pipelines.yml
drwxr-xr-x  16 macports  wheel     512 16 Dec 11:00 cmake
-rwxr-xr-x   1 macports  wheel     418 16 Dec 11:00 configure
drwxr-xr-x   4 macports  wheel     128 16 Dec 11:00 contrib
drwxr-xr-x  11 macports  wheel     352 16 Dec 11:00 doc
drwxr-xr-x   3 macports  wheel      96 16 Dec 11:00 docker
drwxr-xr-x  13 macports  wheel     416 16 Dec 11:00 examples
drwxr-xr-x   8 macports  wheel     256 16 Dec 11:00 genaisrc
drwxr-xr-x   4 macports  wheel     128 16 Dec 11:00 noarch
drwxr-xr-x   4 macports  wheel     128 16 Dec 11:00 resources
drwxr-xr-x  43 macports  wheel    1376 16 Dec 11:00 scripts
drwxr-xr-x  23 macports  wheel     736  7 Mar 16:11 src
-rw-r--r--   1 macports  wheel     352 16 Dec 11:00 z3.pc.cmake.in
-rw-r--r--   1 macports  wheel  126008 16 Dec 11:00 z3guide.jpeg

[lpgaff (Liam Gaffney)]

cmake cache file

[lpgaff (Liam Gaffney)]

Is the clang-19 port installed? Does the clang program it installed work?

Yes clang-19 port is installed and works as expected.

[lpgaff (Liam Gaffney)]

FYI, sudo port install z3-fstar suceeds without a problem. The issues seems to be a missing file /opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_macports_release_tarballs_ports_math_z3/z3/work/z3.profdata, which I cannot find anywhere in the source directories.

I can make it avoid this check completely by using the -pgo option and I also get a successful build.

[ryandesign (Ryan Carsten Schmidt)]

I agree, the z3 port gets the same error on our automated build machines.

Looks like it was intended that the port would extract the profile file from an archive in the files directory, however in the case of the z3 port the archive name that is selected doesn't exist:

:debug:extract Executing proc-post-org.macports.extract-extract-0
:debug:extract system: /opt/local/bin/xz -cd /opt/local/var/macports/sources/rsync.macports.org/macports/release/tarballs/ports/math/z3/files/.profdata.tar.xz | /usr/bin/tar -C /opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_macports_release_tarballs_ports_math_z3/z3/work --no-same-owner -xf -
:info:extract /opt/local/bin/xz: /opt/local/var/macports/sources/rsync.macports.org/macports/release/tarballs/ports/math/z3/files/.profdata.tar.xz: No such file or directory

The Portfile code is:

system "${xz} -cd ${filespath}/${z3.pgo_profile}.profdata.tar.xz | ${tar} -C ${workpath} --no-same-owner -xf -"

So evidently here the ${z3.pgo_profile} variable is unexpectedly empty.

The error is not detected by the extract phase because the error comes from xz and is swallowed up by the pipe (|). tar then receives no input on stdin and evidently considers that to be no problem and exits with the success code (0), so MacPorts proceeds to the configure phase which fails due the missing file that didn't get extracted.

Incidentally, it has been forgotten here to use [shellescape] for all variables that are being used in the system call.

[Chris Jones <jonesc@…>]

In c6d41f796486be89fa1c8f7ebcf3c9797cbdfbe4/macports-ports (master):

z3: Check z3.pgo_profile is properly set before using
See: #72155