#71 closed defect (fixed)

Divine 4.3.2 Build failures

Reported by: imartisko Owned by: mornfall
Priority: major Milestone: 4.3
Component: other Keywords:
Cc: jamartis@…, kdudka@…



I am trying to build the stable version of divine on Fedora 29 but I am running into two problems.

1) The LLVM_CMAKE_PATH variable in the clang/lib/basic/cmakelist.txt does not seem to be set properly during the build which causes the build to fail. When I hardcode the absolute path to llvm/cmake/modulesGetSVN.cmake, the build continues

2) The build fails during the final linking with the error message in the attached file. This only happens when I'm trying to build the release flavour (make release). When building the debug flavour, the build completes successfully.

Attachments (2)

error (5.4 KB) - added by imartisko 22 months ago.
disable-VC-checks.patch (1.5 KB) - added by imartisko 22 months ago.

Download all attachments as: .zip

Change History (5)

Changed 22 months ago by imartisko

Attachment: error added

comment:1 Changed 22 months ago by mornfall

The error from 2) is fixed in the 'next' branch. If you do not want to pull it with darcs, you can apply the following diff locally:

patch c4cc63bfafe279bfb73c1fb8e10b1f837cee5656
Author: Petr Rockai <me@mornfall.net>
Date:   Tue Jul  2 11:40:13 CEST 2019
  * VM: Fix undefined references to context methods (release builds were affected).
diff -rN -u -p old-work/divine/vm/eval.hpp new-work/divine/vm/eval.hpp
--- old-work/divine/vm/eval.hpp	2019-07-02 16:43:36.735786387 +0200
+++ new-work/divine/vm/eval.hpp	2019-07-02 16:43:36.735786387 +0200
@@ -23,6 +23,7 @@
 #include <divine/vm/program.hpp>
 #include <divine/vm/value.hpp>
 #include <divine/vm/context.hpp>
+#include <divine/vm/ctx-debug.tpp>
 #include <divine/vm/divm.h>

As for 1), what is the version of 'cmake' that you are using? Do you have some sort of version control checkout that's not darcs? Seems like the module is only used if version control files exist (which normally don't).

comment:2 Changed 22 months ago by imartisko

Thanks for the patch, it seems to fix the issue 2). As for the issue 1), I have a git repo in the parent directory which seems to indeed be the cause of the problems. I've created a patch that introduces Makefile variable which disables these VC checks if needed (for the tarball versions of the divine, these checks should not be needed, I suppose).

Changed 22 months ago by imartisko

Attachment: disable-VC-checks.patch added

comment:3 Changed 18 months ago by mornfall

Resolution: fixed
Status: newclosed

I have disabled the VC checks unconditionally (we never actually want them anyway).

Note: See TracTickets for help on using tickets.