Opened 5 years ago

Closed 4 years ago

#73 closed defect (fixed)

make install failure - Divine 4.3.2

Reported by: Lukáš Zaoral Owned by: mornfall
Priority: major Milestone: 4.3
Component: other Keywords:



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.

Attachments (2)

error (1.2 KB) - added by Lukáš Zaoral 5 years ago.
make_install.patch (19.8 KB) - added by Lukáš Zaoral 5 years ago.

Download all attachments as: .zip

Change History (14)

Changed 5 years ago by Lukáš Zaoral

Attachment: error added

comment:1 Changed 5 years ago by mornfall

Status: newaccepted

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'.

comment:2 Changed 5 years ago by Lukáš Zaoral

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

1) The 'dios/libcxx/utils/' 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/' 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.

Version 0, edited 5 years ago by Lukáš Zaoral (next)

Changed 5 years ago by Lukáš Zaoral

Attachment: make_install.patch added

comment:3 Changed 5 years ago by 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.

comment:4 Changed 5 years ago by 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.

comment:5 Changed 5 years ago by mornfall

Resolution: fixed
Status: acceptedclosed

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.

comment:6 Changed 5 years ago by Lukáš Zaoral

Resolution: fixed
Status: closedreopened

I have just tried clean building the latest nightly release and make install still fails because of invalid permissions on the 'dios/libcxx/utils/' 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/ /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/ Permission denied

comment:7 Changed 4 years ago by 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?

comment:8 Changed 4 years ago by 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.

comment:9 Changed 4 years ago by 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_CXX_ABI "libcxxabi" CACHE STRING "" )
+  include( FindPythonInterp )
   add_subdirectory( ${dir}/libcxxabi )
   add_subdirectory( ${dir}/libcxx )

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

comment:10 Changed 4 years ago by Lukáš Zaoral

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

[40/40] Creating library symlink lib/ lib/
FAILED: lib/ lib/
/usr/bin/cmake -E cmake_symlink_library lib/  lib/ lib/ && cd /home/lukas/divine/python_test/_build.toolchain/dios/libcxx/src && /usr/bin/python /home/lukas/divine/python_test/dios/libcxx/utils/ --input /home/lukas/divine/python_test/_build.toolchain/lib/ --output /home/lukas/divine/python_test/_build.toolchain/lib/ unwind c++abi
/usr/bin/python: can't open file '/home/lukas/divine/python_test/dios/libcxx/utils/': [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

comment:11 Changed 4 years ago by 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.

comment:12 Changed 4 years ago by mornfall

Resolution: fixed
Status: reopenedclosed

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

Note: See TracTickets for help on using tickets.