make install failure - Divine 4.3.2

[Lukáš Zaoral]

Hi,

I am trying to build divine 4.3.2 on Fedora 30. The build itself is fine (after applying patch in #71), but the subsequent installation fails because of a missing file in includes. The problem persists even with the latest nightly build. The error message is attached.

[mornfall]

Yes, sorry, the install target is not exactly maintained (partly because we build LLVM and also need to install that, which might mess up a different LLVM installation in the same prefix). What we usually do is build static binaries, which are standalone and can be installed with 'cp'. That said, I'll look into fixing 'make install'.

[Lukáš Zaoral]

I was able to successfully install the latest release of Divine on Fedora 30 with following modifications:

1) The 'dios/libcxx/utils/cat_files.py' script should have the executable bit set.

2) The 'DarwinLdOptions?.inc' file is missing from the include directories of lld.
Creating a symbolic link from '_build.toolchain/lld/lib/Driver/DarwinLdOptions.inc' to one of these directories solves the issue.

3) The 'gtest-dev' package must be installed to resolve linking problems.

The attached patch contains following modifications:

4) Assuming a user without root privileges, all occurrences of the PWD variable in the main Makefile should be replaced with a CURDIR directive, because running make install (or anything else) with sudo with no options (like -E) does not preserve this variable and cmake fails.

5) The 'stp/lib/Interface/CMakeLists.txt' file has a wrong source path for installation of headers on line 43. '/include' should be 'stp/include'.

6) The 'releng/install-rpath.cmake' is outdated to be used with latest Divine builds.

7) The 'divine/CMakeLists.txt' file has missing install targets for divine-sim, divine-mc, divine-smt and divine-dbg.

Few of these modifications are more of a workaround than fix, but I hope they point to the right direction.

[Lukáš Zaoral]

After the refactor of brick-cmd, the 4.3.5 release of Divine needs one additional change for a successful installation. The occurrences of the make_option_set method in 'tools/divcheck.hpp' should no longer be templated.

[Lukáš Zaoral]

The issue with divcheck compilation is fixed in 4.3.6, but 7) is fixed only partially, the install command for divine-sim target is still missing. Thanks.

[mornfall]

I have applied your install-rpath changes and fixed the remaining issues one way or another. The install still fails without libgtest-dev and it's not entirely clear how to go about fixing that. The results are also still quite messy and a whole bunch of headers is missing, but as of this writing, the target runs to the end on next and the installed binaries seem to work.

[Lukáš Zaoral]

I have just tried clean building the latest nightly release and make install still fails because of invalid permissions on the 'dios/libcxx/utils/cat_files.py' script. On the other hand, everything else seems to be fixed, which is great!

[1/673] Generating ../__generated_config
FAILED: dios/libcxx/__generated_config 
cd /home/lukas/divine/divine-4.3.9+2019.10.20/_build.toolchain/dios/libcxx/include && /home/lukas/divine/divine-4.3.9+2019.10.20/dios/libcxx/utils/cat_files.py /home/lukas/divine/divine-4.3.9+2019.10.20/_build.toolchain/dios/libcxx/__config_site /home/lukas/divine/divine-4.3.9+2019.10.20/dios/libcxx/include/__config -o /home/lukas/divine/divine-4.3.9+2019.10.20/_build.toolchain/dios/libcxx/__generated_config
/bin/sh: /home/lukas/divine/divine-4.3.9+2019.10.20/dios/libcxx/utils/cat_files.py: Permission denied

[mornfall]

The permissions are correct, the script should not be executed directly, but passed to python. Can you check what your PYTHON_EXECUTABLE is set to, in CMakeCache.txt?

[Lukáš Zaoral]

The PYTHON_EXECUTABLE variable in CMakeCache.txt is correctly set to /usr/bin/python. However, this variable is set by CMake after the configuration of libcxx. Therefore, the code on line 184 in 'dios/libcxx/include/CMakeLists.txt' evaluates to the command mentioned in my comment above.

Not the nicest solution, but if I add include(FindPythonInterp) just before this line, everything seems to work as it should.

[mornfall]

diff -rN -u -p old-work/CMakeLists.txt new-work/CMakeLists.txt
--- old-work/CMakeLists.txt	2019-12-18 14:49:06.589223299 +0100
+++ new-work/CMakeLists.txt	2019-12-18 14:49:06.589223299 +0100
@@ -113,6 +113,7 @@ function( build_libcxx dir )
   set( LIBCXX_ABI_VERSION 2 CACHE STRING "" )
   set( LIBCXX_CXX_ABI "libcxxabi" CACHE STRING "" )
   set( LIBCXX_CXX_ABI_INTREE ON CACHE BOOL "" )
+  include( FindPythonInterp )
   add_subdirectory( ${dir}/libcxxabi )
   add_subdirectory( ${dir}/libcxx )
 endfunction()

Can you perhaps check that the above patch fixes the problem for you?

[Lukáš Zaoral]

Unfortunately, with your patch the build of libcxx fails due to a missing file:

[40/40] Creating library symlink lib/libc++.so.2 lib/libc++.so
FAILED: lib/libc++.so.2 lib/libc++.so
/usr/bin/cmake -E cmake_symlink_library lib/libc++.so.2.0  lib/libc++.so.2 lib/libc++.so && cd /home/lukas/divine/python_test/_build.toolchain/dios/libcxx/src && /usr/bin/python /home/lukas/divine/python_test/dios/libcxx/utils/gen_link_script.py --input /home/lukas/divine/python_test/_build.toolchain/lib/libc++.so.2 --output /home/lukas/divine/python_test/_build.toolchain/lib/libc++.so unwind c++abi
/usr/bin/python: can't open file '/home/lukas/divine/python_test/dios/libcxx/utils/gen_link_script.py': [Errno 2] No such file or directory
ninja: build stopped: subcommand failed.
make[1]: *** [Makefile:138: /home/lukas/divine/python_test/_build.toolchain/stamp-v8] Error 1
make: *** [Makefile:76: release] Error 2

[Lukáš Zaoral]

I have just tried the 4.4.1 release of Divine and the make install target now additionally fails during compilation of the shoop.cpp file.

[mornfall]

Should be fixed in next (please create new tickets for regressions in the future).