[SATLUG] Re: Prover9 problem
mauricejfox at gmail.com
Sun May 13 14:04:30 CDT 2012
After some fiddling around with gcc, nm, and whatnot, here's the solution, strange though it may be.
On ubuntu, if test is a program calling for round and ceil, in C and C++ versions
g++ -o test -lm test.cpp
gcc -o test -lm test.c
But if I move the -lm parameter like this
gcc -o test test.c -lm
it works OK. (It also works OK on t he g++ line to move -lm to the end.)
So the problem was in the Makefile. I edited the Makefile to move -lm after the source/object lists, and everything built OK. For some reason gcc version 4.6.3 as distributed with the most recent ubuntu this way. The inconsistency between gcc and g++ is a little strange. Seems that both invoke ld, but what do I know?
On May 12, 2012, at 12:00 PM, satlug-request at satlug.org wrote:
> Message: 2
> Date: Fri, 11 May 2012 13:39:12 -0500
> From: Maurice Fox <mauricejfox at gmail.com>
> Subject: [SATLUG] Prover9 problem
> To: satlug at satlug.org
> Message-ID: <AF0A3278-FC80-4E20-9FD4-4A433BF006D7 at gmail.com>
> Content-Type: text/plain; charset=us-ascii
> I downloaded the automated theorem prover called Prover9 from its home page and tried to build it under the most recent Ubuntu distro. It failed on two unresolved symbols in ld: ceil and round.
> I moved the tar.gz file over to Mac OS X LION, extracted the source files, and built it just fine. Ran the tests under make test, completely successful.
> Anybody have any idea why the Linux distro would not resolve those two calls? They should be part of libm.a, and indeed running ar on libm.a reveals that t here is related content. For ceil, I get s_ceil.a, s_ceill.a, and s_ceilf.a. Similarly, for round, I get nine variously decorated .o files.
> Any ideas?
More information about the SATLUG