make: CMake does not set PYTHON_INTERP during libcxx configuration

[Lukáš Zaoral]

Hi, as previously discussed in the comments 6-10 of issue #73, the make install target still fails to complete without some additional downstream patching. This issue occurs on Fedora, Manjaro, Ubuntu (and probably on other Linux distros too). Thanks.

[Vladimír Štill]

I was able to reproduce this on Archlinux, the problem occurs only in make install, apparently in the toolchain part of the install.

$ make install PREFIX=/tmp/divine JOBS=1                                                                                       
[1/648] Generating ../__generated_config                                                                                          
FAILED: dios/libcxx/__generated_config                                                                                            
cd /var/obj/xstill-divine-interp/toolchain/dios/libcxx/include && /tmp/interp/dios/libcxx/utils/cat_files.py /var/obj/xstill-divin|
e-interp/toolchain/dios/libcxx/__config_site /tmp/interp/dios/libcxx/include/__config -o /var/obj/xstill-divine-interp/toolchain/d
ios/libcxx/__generated_config                                                                                                     
/bin/sh: /tmp/interp/dios/libcxx/utils/cat_files.py: Permission denied
ninja: build stopped: subcommand failed.
make: *** [Makefile:164: toolchain-install] Error 1

[Lukáš Zaoral]

This particular problem seems to be fixed in 4.4.2. However, it introduced another one in the final phase of toolchain installation. The gen_link_script.py script replaces libc++.so with a plaintext file containing instructions for linker, but CMake expects that this file is in an ELF format.

-- Installing: /opt/divine/lib/libc++.so.2
-- Set runtime path of "/opt/divine/lib/libc++.so.2.0" to "/opt/divine/lib"
-- Installing: /opt/divine/lib/libc++.so
CMake Error at dios/libcxx/src/cmake_install.cmake:83 (file):
  file RPATH_CHANGE could not write new RPATH:

    /opt/divine/lib

  to the file:

    /opt/divine/lib/libc++.so

  No valid ELF RPATH or RUNPATH entry exists in the file; File does not have
  a valid ELF identification.
Call Stack (most recent call first):
  dios/libcxx/cmake_install.cmake:51 (include)
  cmake_install.cmake:44 (include)


FAILED: CMakeFiles/install.util 
cd /builds/lzaoral/divine/_build.toolchain && /usr/bin/cmake -P cmake_install.cmake
ninja: build stopped: subcommand failed.
make: *** [Makefile:164: install] Error 1

[chenminglei]

How did you solve the last mentioned problem above, I am meeting the same one.

[Lukáš Zaoral]

I've used the following patch. Unfortunately, this issue tracker seems to be rather dead and iirc the last activity by Divine's authors here was in 2020.

diff -u a/dios/libcxx/CMakeLists.txt b/dios/libcxx/CMakeLists.txt
--- a/dios/libcxx/CMakeLists.txt
+++ b/dios/libcxx/CMakeLists.txt
@@ -214,13 +214,13 @@ cmake_dependent_option(LIBCXX_STATICALLY_LINK_ABI_IN_SHARED_LIBRARY
 # is on. This option is also disabled when the ABI library is not specified
 # or is specified to be "none".
 set(ENABLE_LINKER_SCRIPT_DEFAULT_VALUE OFF)
-if (LLVM_HAVE_LINK_VERSION_SCRIPT AND NOT LIBCXX_STATICALLY_LINK_ABI_IN_SHARED_LIBRARY
-      AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "none"
-      AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "default"
-      AND PYTHONINTERP_FOUND
-      AND LIBCXX_ENABLE_SHARED)
-    set(ENABLE_LINKER_SCRIPT_DEFAULT_VALUE ON)
-endif()
+# if (LLVM_HAVE_LINK_VERSION_SCRIPT AND NOT LIBCXX_STATICALLY_LINK_ABI_IN_SHARED_LIBRARY
+#       AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "none"
+#       AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "default"
+#       AND PYTHONINTERP_FOUND
+#       AND LIBCXX_ENABLE_SHARED)
+#     set(ENABLE_LINKER_SCRIPT_DEFAULT_VALUE ON)
+# endif()

[Dávid Bolvanský]

There is an ongoing development of new divine. We do not use cmake anymore.

Not sure if this version (4.4.2) is still supported - if yes, we should take your patch..

[Lukáš Zaoral]

Yes, I know that Divine is being developed again for a few months now (that's why I specified that the "issue tracker seems dead" not the whole project ;) ). However, that does not change the fact that (almost?) all issues that were reported in the last two years, either by me or others, were ignored and were left without any input or acknowledgement from Divine's side.

[chenminglei]

Replying to Dávid Bolvanský:

There is an ongoing development of new divine. We do not use cmake anymore.
Thanks for you a lot! It still works for divine-4.4.2.
Not sure if this version (4.4.2) is still supported - if yes, we should take your patch..