[CMake] Make pkg-config metadata relocatable (#10734)

The old pkg-config files didn't support relocation, which makes
packaging difficult. They also didn't support static linking. This PR
fixes both issues by referencing by computing a prefix relative to
`${pcfiledir}` and adding `.private` metadata to `z3.pc`.

.github/workflows/ci.yml

@@ -454,6 +454,19 @@ jobs:
           cmake --build build --target libz3 shell
           cmake --install build --prefix "$PWD/install"
 
+      - name: Consume relocated static pkg-config package
+        run: |
+          cp -a install install-relocated
+          export PKG_CONFIG_PATH="$PWD/install-relocated/lib/pkgconfig"
+          c++ cmake/tests/package/package_test.cpp \
+            $(pkg-config --cflags --libs --static z3) \
+            -static \
+            -o pkg-config-test
+          ./pkg-config-test
+
+          # Confirm the binary has no dynamic library dependencies at all.
+          ! ldd pkg-config-test
+
       - name: Build Python bindings from installed shared package
         run: |
           cmake -S . -B build-python-only -G Ninja \

CMakeLists.txt

@@ -670,8 +670,42 @@ configure_file(
 )
 unset(Z3_FIND_GMP_MODULE_DIR)
 
-configure_file("${CMAKE_CURRENT_SOURCE_DIR}/z3.pc.cmake.in"
-  "${CMAKE_CURRENT_BINARY_DIR}/z3.pc" @ONLY)
+if (Z3_BUILD_LIBZ3_CORE)
+  set(Z3_PKGCONFIG_DIR "${CMAKE_INSTALL_PKGCONFIGDIR}")
+  get_filename_component(Z3_PKGCONFIG_DIR "${Z3_PKGCONFIG_DIR}" ABSOLUTE
+    BASE_DIR "${CMAKE_INSTALL_PREFIX}")
+  set(Z3_PKGCONFIG_PREFIX "${CMAKE_INSTALL_PREFIX}")
+  file(RELATIVE_PATH Z3_PKGCONFIG_PREFIX
+    "${Z3_PKGCONFIG_DIR}" "${Z3_PKGCONFIG_PREFIX}")
+
+  set(Z3_PKGCONFIG_REQUIRES_PRIVATE "")
+  if (Z3_USE_LIB_GMP)
+    set(Z3_PKGCONFIG_REQUIRES_PRIVATE gmp)
+  endif()
+
+  set(Z3_PKGCONFIG_LIBS_PRIVATE "")
+  if (CMAKE_THREAD_LIBS_INIT)
+    list(APPEND Z3_PKGCONFIG_LIBS_PRIVATE "${CMAKE_THREAD_LIBS_INIT}")
+  endif()
+  if (ATOMICS_REQUIRE_LIBATOMIC)
+    list(APPEND Z3_PKGCONFIG_LIBS_PRIVATE -latomic)
+  endif()
+  if (MINGW)
+    list(APPEND Z3_PKGCONFIG_LIBS_PRIVATE -ldbghelp)
+  endif()
+  foreach (implicit_lib IN LISTS CMAKE_CXX_IMPLICIT_LINK_LIBRARIES)
+    if (implicit_lib MATCHES "^(c\\+\\+|stdc\\+\\+|m)$")
+      list(APPEND Z3_PKGCONFIG_LIBS_PRIVATE "-l${implicit_lib}")
+    endif()
+  endforeach()
+  list(REMOVE_DUPLICATES Z3_PKGCONFIG_LIBS_PRIVATE)
+  list(JOIN Z3_PKGCONFIG_LIBS_PRIVATE " " Z3_PKGCONFIG_LIBS_PRIVATE)
+
+  configure_file("${CMAKE_CURRENT_SOURCE_DIR}/z3.pc.cmake.in"
+    "${CMAKE_CURRENT_BINARY_DIR}/z3.pc.configured" @ONLY)
+  file(GENERATE OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/z3.pc"
+    INPUT "${CMAKE_CURRENT_BINARY_DIR}/z3.pc.configured")
+endif()
 
 ################################################################################
 # Create `Z3Config.cmake` and related files for install tree so clients can use

z3.pc.cmake.in

@@ -1,13 +1,13 @@
-prefix=@CMAKE_INSTALL_PREFIX@
-exec_prefix=@CMAKE_INSTALL_PREFIX@
+prefix=${pcfiledir}/@Z3_PKGCONFIG_PREFIX@
+exec_prefix=${prefix}
 libdir=${exec_prefix}/@CMAKE_INSTALL_LIBDIR@
-sharedlibdir=${exec_prefix}/@CMAKE_INSTALL_LIBDIR@
 includedir=${prefix}/@CMAKE_INSTALL_INCLUDEDIR@
 
 Name: z3
 Description: The Z3 Theorem Prover
 Version: @Z3_VERSION@
 
-Requires:
-Libs: -L${libdir} -L${sharedlibdir} -lz3
+Requires.private: @Z3_PKGCONFIG_REQUIRES_PRIVATE@
+Libs: -L${libdir} -l$<TARGET_FILE_BASE_NAME:z3::libz3>
+Libs.private: @Z3_PKGCONFIG_LIBS_PRIVATE@
 Cflags: -I${includedir}