Linking Error - Githubissues

soonhokong commented 9 years ago

@zenna reported to @scungao.

On Thu, Jan 22, 2015 at 10:47 PM, Zenna Tavares <zennatavares@gmail.com> wrote:
> /home/zenna/repos/dreal_nra/build/release/lib/libglog.a(libglog_la-utilities.o):
> In function `google::GetStackTrace(void**, int, int)':
> /home/zenna/repos/dreal_nra/build/release/external/src/GLOG/src/stacktrace_libunwind-inl.h:65:
> undefined reference to `_Ux86_64_getcontext'
> /home/zenna/repos/dreal_nra/build/release/external/src/GLOG/src/stacktrace_libunwind-inl.h:66:
> undefined reference to `_ULx86_64_init_local'
> /home/zenna/repos/dreal_nra/build/release/external/src/GLOG/src/stacktrace_libunwind-inl.h:78:
> undefined reference to `_ULx86_64_step'
> /home/zenna/repos/dreal_nra/build/release/external/src/GLOG/src/stacktrace_libunwind-inl.h:70:
> undefined reference to `_ULx86_64_get_reg'
> /home/zenna/repos/dreal_nra/build/release/lib/libCoinUtils.so: undefined
> reference to `dgetrf_'
> /home/zenna/repos/dreal_nra/build/release/lib/libCoinUtils.so: undefined
> reference to `dgetrs_'
> collect2: error: ld returned 1 exit status
> make[2]: *** [dReal] Error 1
> make[1]: *** [CMakeFiles/dReal.dir/all] Error 2
> make: *** [all] Error 2
>

soonhokong commented 9 years ago

https://code.google.com/p/google-glog/issues/detail?id=207

soonhokong commented 9 years ago

@zenna and @scungao, I've updated soonhokong/glog repository which is used in dReal build process. Could you go to your build directory, do the followings, let me know if it fixes your problem?

rm -rf external
ninja # or make

zenna commented 9 years ago

@soonhokong No, it didn't; the build still fails.

Neither did a rebuilding everything from scratch help. I should point out that these linking errors occur when dReal is being linked, .i.e.

[  8%] Built target CAPD4
[ 16%] Built target GFLAGS
[ 25%] Built target GLOG
[ 33%] Built target GTEST
[ 42%] Built target IBEX
[ 50%] Built target JSON11
[ 60%] Built target util
[ 67%] Built target opensmt_egraph
[ 69%] Built target opensmt_cnfizers
[ 70%] Built target opensmt_common
[ 74%] Built target opensmt_smt2parser
[ 83%] Built target opensmt_simplifiers
[ 90%] Built target opensmt_smtsolvers
[ 92%] Built target opensmt_sorts
[ 93%] Built target opensmt_tsolvers
[ 94%] Built target opensmt_emptysolver
[ 95%] Built target dsolvers
[ 97%] Built target opensmt_api
Linking CXX executable dReal
/home/zenna/repos/dreal_nra/build/lib/libglog.a(libglog_la-utilities.o): In function `google::GetStackTrace(void**, int, int)':
/home/zenna/repos/dreal_nra/build/external/src/GLOG/src/stacktrace_libunwind-inl.h:65: undefined reference to `_Ux86_64_getcontext'
/home/zenna/repos/dreal_nra/build/external/src/GLOG/src/stacktrace_libunwind-inl.h:66: undefined reference to `_ULx86_64_init_local'
/home/zenna/repos/dreal_nra/build/external/src/GLOG/src/stacktrace_libunwind-inl.h:78: undefined reference to `_ULx86_64_step'
/home/zenna/repos/dreal_nra/build/external/src/GLOG/src/stacktrace_libunwind-inl.h:70: undefined reference to `_ULx86_64_get_reg'
/home/zenna/repos/dreal_nra/build/lib/libCoinUtils.so: undefined reference to `dgetrf_'
/home/zenna/repos/dreal_nra/build/lib/libCoinUtils.so: undefined reference to `dgetrs_'
collect2: error: ld returned 1 exit status
make[2]: *** [dReal] Error 1
make[1]: *** [CMakeFiles/dReal.dir/all] Error 2
make: *** [all] Error 2

soonhokong commented 9 years ago

@zenna, thanks for the report. Let me reproduce the problem on my machine. I'll be right back.

soonhokong commented 9 years ago

@zenna, could you let me know if your system has any of the following packages installed?

libunwind-setjmp0 - A libunwind-based non local goto - runtime
libunwind-setjmp0-dev - A libunwind-based non local goto - development
libunwind7 - A library to determine the call-chain of a program - runtime
libunwind7-dev - A library to determine the call-chain of a program - development

soonhokong commented 9 years ago

It seems that I find the problem. When glog is built using libunwind, we need to pass -lunwind linker flag for dReal. For now, this step is missing. I'll add it soon.

soonhokong commented 9 years ago

@zenna, could you try the latest version and let me know if it fixes your problem?

I was able to reproduce the problem on my system and then 96b6cec5cadc9d614bda6f27feaf80c2263b2188 fixed the problem on my system.

zenna commented 9 years ago

I tried the newest version. First of all I got Ocaml errors saying I did not have batteries installed so I installed libbatteries-ocaml-dev. I then did a fresh install and got

ocaml setup.ml -build Finished, 1 target (0 cached) in 00:00:00.

ocamlfind ocamlc -c -g -package batteries -I basic -o basic/hybrid.cmo basic/hybrid.ml File "basic/hybrid.ml", line 82, characters 25-32: Warning 40: jumpmap was selected from type Mode.t. It is not visible in the current scope, and will not be selected if the type becomes unknown.
ocamlfind ocamlopt -c -g -passopt -annot -package batteries -I basic -o basic/hybrid.cmx basic/hybrid.ml File "basic/hybrid.ml", line 82, characters 25-32: Warning 40: jumpmap was selected from type Mode.t. It is not visible in the current scope, and will not be selected if the type becomes unknown.
ocamlfind ocamlc -c -g -I basic -package batteries -I heuristic -I basic -o heuristic/heuristic.cmo heuristic/heuristic.ml File "heuristic/heuristic.ml", line 61, characters 4-5: Warning 11: this match case is unused. File "heuristic/heuristic.ml", line 352, characters 8-21: Warning 26: unused variable goal_mode_ids. File "heuristic/heuristic.ml", line 378, characters 8-20: Warning 26: unused variable init_mode_id.
ocamlfind ocamlopt -c -g -I basic -passopt -annot -package batteries -I heuristic -I basic -o heuristic/heuristic.cmx heuristic/heuristic.ml File "heuristic/heuristic.ml", line 61, characters 4-5: Warning 11: this match case is unused. File "heuristic/heuristic.ml", line 352, characters 8-21: Warning 26: unused variable goal_mode_ids. File "heuristic/heuristic.ml", line 378, characters 8-20: Warning 26: unused variable init_mode_id.
/usr/bin/ocamlyacc parsing/drh_parser.mly 2 rules never reduced 76 shift/reduce conflicts, 6 reduce/reduce conflicts. 00:00:05 84 (0 ) invariant-checking/src/inv_check.cmx ONb--Dil [15105:15146:0124/035405:ERROR:channel.cc(290)] RawChannel read error (connection broken)
/usr/bin/ocamlyacc smt2/smt2parser.mly 87 shift/reduce conflicts, 2 reduce/reduce conflicts. Finished, 107 targets (0 cached) in 00:00:08.

I ran build.sh again and got

-- Configuring incomplete, errors occurred!
See also "/home/zenna/repos/dreal_nra/build/CMakeFiles/CMakeOutput.log".
You have changed variables that require your cache to be deleted.
Configure will be re-run and you may have to reset some variables.
The following variables have changed:
CMAKE_C_COMPILER= gcc-4.8
CMAKE_CXX_COMPILER= g++-4.8

-- Generating done
-- Build files have been written to: /home/zenna/repos/dreal_nra/build
-- The C compiler identification is GNU 4.8.2
-- The CXX compiler identification is GNU 4.8.2
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Found Git: /usr/local/bin/git  
-- Found BISON: /usr/bin/bison (found version "3.0.2") 
-- Found FLEX: /usr/bin/flex (found version "2.5.35") 
CMake Error at cmake/Modules/FindLibunwind.cmake:19 (message):
  libunwind.h found without matching unwind.h
Call Stack (most recent call first):
  CMakeLists.txt:121 (find_package)

Sorry I can't be of more help, I'm writing a paper right now.

soonhokong commented 9 years ago

@zenna

OCaml problem is a different issue. We're using a pretty recent version of OCaml (4.01.0) which is hard to install via apt-get. We recommend users to install OCaml via opam and I put detailed instructions at https://github.com/dreal/dreal/blob/master/doc/ubuntu-gcc.md#dreachbmc-and-other-tools
I just pushed a new commit to dreal/dreal_nra repo. Could you git pull and do the following?

cd /home/zenna/repos/dreal_nra/build
make

Sorry I can't be of more help, I'm writing a paper right now.

You're very helpful! Thanks for the time and good luck with the submission!

scungao commented 9 years ago

Zenna doesn't need the ocaml part. We should really separate the dreal and dreach building.

On Jan 24, 2015, at 04:19, Soonho Kong notifications@github.com wrote:

@zenna

OCaml problem is a different issue. We're using a pretty recent version of OCaml (4.01.0) which is hard to install via apt-get. We recommend users to install OCaml via opam and I put detailed instructions at https://github.com/dreal/dreal/blob/master/doc/ubuntu-gcc.md#dreachbmc-and-other-tools

I just pushed a new commit to dreal/dreal_nra repo. Could you git pull and do the following?

cd /home/zenna/repos/dreal_nra/build make Sorry I can't be of more help, I'm writing a paper right now.

You're very helpful! Thanks for the time and good luck with the submission!

— Reply to this email directly or view it on GitHub.

scungao commented 9 years ago

Also let's make a "test" release binary on the new nra branch so that it's easier for others to try.

On Jan 24, 2015, at 04:19, Soonho Kong notifications@github.com wrote:

@zenna

OCaml problem is a different issue. We're using a pretty recent version of OCaml (4.01.0) which is hard to install via apt-get. We recommend users to install OCaml via opam and I put detailed instructions at https://github.com/dreal/dreal/blob/master/doc/ubuntu-gcc.md#dreachbmc-and-other-tools

I just pushed a new commit to dreal/dreal_nra repo. Could you git pull and do the following?

cd /home/zenna/repos/dreal_nra/build make Sorry I can't be of more help, I'm writing a paper right now.

You're very helpful! Thanks for the time and good luck with the submission!

— Reply to this email directly or view it on GitHub.

zenna commented 9 years ago

@soonhokong No change. I still get

Linking CXX executable dReal
/home/zenna/repos/dreal_nra/build/lib/libCoinUtils.so: undefined reference to `dgetrf_'
/home/zenna/repos/dreal_nra/build/lib/libCoinUtils.so: undefined reference to `dgetrs_'

Of the libraries you suggested, I have none installed. I have libunwind8 and libunwind8-dev. I am on ubuntu 14.04.

soonhokong commented 9 years ago

@zenna, thanks for the information. It seems that at least we don't have the problem with libunwind.

The new problem indicates that you have LAPACK installed and Coin library on which dReal depends uses the system LAPACK instead of its third party one. However, when dReal is built, we don't link the system LAPACK and that is why we have the problem.

@scungao is right. I'll try to prepare a static binary (or a binary with minimal so dependencies) so that you can focus on your research). In the meantime, I'll keep digging to fix the problem (dgetrf_ and dgetrs_)

soonhokong commented 9 years ago

@zenna and @scungao, thanks for waiting. I've managed to make a static binary for the new version. Please download it and let me know if it doesn't work on your system:

https://dl.dropboxusercontent.com/u/10377018/dReal

@scungao, I've made the following changes:

dReal builds a static library of Clp (linear solving library on which IBEX depends) instead of letting IBEX builds Clp by itself. This way, we can take things under our control. Note that Clp itself has dependencies including Lapack and Blas. Even if a system has a system-wide library, we enforce Clp to build its own Lapack and Blas to include them in the static library. @zenna's second problem was caused by Clp uses the system library Lapack.
Then, we let IBEX uses the Clp that we just built.

zenna commented 9 years ago

@soonhokong Thanks! the binary seems to work. In the output of the new version I noticed in the summary details 'Number of Pop'. Does this imply that I can use the new version incrementally? currently I am sending many (thousands) of requests to solvers (through the file interface) which vary only by a few constraints. Is there currently a way to do this which would be substantially more performant?

soonhokong commented 9 years ago

@zenna, good to know that at least the binary is working. Could you actually check out the latest source code and test cd /home/zenna/repos/dreal_nra/build && make? I'm wondering whether the recent patches fix your problem or not.

In the output of the new version I noticed in the summary details 'Number of Pop'.

FYI, those stat messages are there for debugging purposes. I will provide an option to show them.

Does this imply that I can use the new version incrementally? currently I am sending many (thousands) of requests to solvers (through the file interface) which vary only by a few constraints. Is there currently a way to do this which would be substantially more performant?

Incremental solving is on our to-do list. Ideally, you can use dReal via its C API as https://github.com/dreal/dreal_nra/blob/master/src/tests/c_api/example_01.c does so. For now, we do have some problems and it doesn't work yet.

For SAT case, it should return a model in intervals, which is not done right.
Incremental solving is not properly implemented yet. The performance must not be good yet.

Once I finish the two items, I'll let you know.

zenna commented 9 years ago

@soonhokong It builds! (aside from the ocaml issues which I haven't resolved).

To clarify when you say "For now, we do have some problems and it doesn't work yet." do you mean this build in general, or using the C API?

soonhokong commented 9 years ago

@zenna, first of all, thanks for checking this for us. I feel much better now!

To clarify when you say "For now, we do have some problems and it doesn't work yet." do you mean this build in general, or using the C API?

I meant that there are some problems in using dReal via C APIs. The binary is working even if there are some known bugs (different ones).

Let me close this issue because it seems that we resolved the linkage problem. Please subscribe #3, to get notification about it.

scungao commented 9 years ago

We haven't really worked out how to do nonlinear solving incrementally. It's hard to balance efficiency and incrementality. So I'd say it doesn't work at all yet.

On Jan 26, 2015, at 17:49, Zenna Tavares notifications@github.com wrote:

@soonhokong It builds! (aside from the ocaml issues which I haven't resolved).

To clarify when you say "For now, we do have some problems and it doesn't work yet." do you mean this build in general, or using the C API?

— Reply to this email directly or view it on GitHub.

dreal / dreal3

Linking Error #1