I am trying to install the automated theorem prover prover9 on Ubuntu 20.10. So I went to this page and downloaded the file "LADR-2009-11A.tar.gz". Then, I followed the instructions on this page and executed the lines
zcat LADR-2009-11A.tar.gz | tar xvf -
cd LADR-2009-11A
make all
Unfortunately, the third line results in an error: "undefined reference to round" (I think).
The full output message is here:
~/Downloads/LADR-2009-11A$ make all
cd ladr && make lib
make[1]: Entering directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make libladr.a
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make[2]: 'libladr.a' is up to date.
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make[1]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/ladr'
cd mace4.src && make all
make[1]: Entering directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
cd ../ladr && make libladr.a
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make[2]: 'libladr.a' is up to date.
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make clean
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
/bin/rm -f *.o
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
make libmace4.a
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
gcc -O -Wall -c -o estack.o estack.c
gcc -O -Wall -c -o util.o util.c
gcc -O -Wall -c -o print.o print.c
print.c: In function ‘p_model’:
print.c:114:6: warning: format not a string literal and no format arguments [-Wformat-security]
114 | printf(s2);
| ^~~~~~
print.c:119:8: warning: format not a string literal and no format arguments [-Wformat-security]
119 | printf(s3);
| ^~~~~~
print.c:137:4: warning: format not a string literal and no format arguments [-Wformat-security]
137 | printf(s2);
| ^~~~~~
print.c:145:8: warning: format not a string literal and no format arguments [-Wformat-security]
145 | printf(s3);
| ^~~~~~
gcc -O -Wall -c -o syms.o syms.c
gcc -O -Wall -c -o ground.o ground.c
gcc -O -Wall -c -o arithmetic.o arithmetic.c
gcc -O -Wall -c -o select.o select.c
select.c: In function ‘select_concentric_band’:
select.c:236:5: warning: type of ‘min_id’ defaults to ‘int’ [-Wimplicit-int]
236 | int select_concentric_band(min_id, max_id, max_constrained)
| ^~~~~~~~~~~~~~~~~~~~~~
select.c:236:5: warning: type of ‘max_id’ defaults to ‘int’ [-Wimplicit-int]
select.c:236:5: warning: type of ‘max_constrained’ defaults to ‘int’ [-Wimplicit-int]
gcc -O -Wall -c -o propagate.o propagate.c
gcc -O -Wall -c -o mstate.o mstate.c
gcc -O -Wall -c -o negpropindex.o negpropindex.c
gcc -O -Wall -c -o negprop.o negprop.c
gcc -O -Wall -c -o ordercells.o ordercells.c
gcc -O -Wall -c -o commandline.o commandline.c
gcc -O -Wall -c -o msearch.o msearch.c
msearch.c: In function ‘next_domain_size’:
msearch.c:850:5: warning: type of ‘n’ defaults to ‘int’ [-Wimplicit-int]
850 | int next_domain_size(n)
| ^~~~~~~~~~~~~~~~
ar rs libmace4.a estack.o util.o print.o syms.o ground.o arithmetic.o select.o propagate.o mstate.o negpropindex.o negprop.o ordercells.o commandline.o msearch.o
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
gcc -O -Wall -c -o mace4.o mace4.c
mace4.c: In function ‘init_attrs’:
mace4.c:36:7: warning: variable ‘id’ set but not used [-Wunused-but-set-variable]
36 | int id;
| ^~
gcc -O -Wall -o mace4 mace4.o libmace4.a ../ladr/libladr.a
/bin/mv mace4 ../bin
make[1]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
cd provers.src && make all
make[1]: Entering directory '/home/utente/Downloads/LADR-2009-11A/provers.src'
cd ../ladr && make libladr
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make libladr.a
make[3]: Entering directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make[3]: 'libladr.a' is up to date.
make[3]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/ladr'
make clean
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/provers.src'
/bin/rm -f *.o
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/provers.src'
cd ../mace4.src && make libmace4
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
make libmace4.a
make[3]: Entering directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
make[3]: 'libmace4.a' is up to date.
make[3]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/mace4.src'
make clean
make[2]: Entering directory '/home/utente/Downloads/LADR-2009-11A/provers.src'
/bin/rm -f *.o
make[2]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/provers.src'
gcc -O -Wall -c -o prover9.o prover9.c
gcc -O -Wall -c -o index_lits.o index_lits.c
gcc -O -Wall -c -o forward_subsume.o forward_subsume.c
gcc -O -Wall -c -o demodulate.o demodulate.c
gcc -O -Wall -c -o pred_elim.o pred_elim.c
gcc -O -Wall -c -o unfold.o unfold.c
gcc -O -Wall -c -o semantics.o semantics.c
gcc -O -Wall -c -o giv_select.o giv_select.c
gcc -O -Wall -c -o white_black.o white_black.c
gcc -O -Wall -c -o actions.o actions.c
gcc -O -Wall -c -o search.o search.c
gcc -O -Wall -c -o utilities.o utilities.c
gcc -O -Wall -c -o provers.o provers.c
gcc -O -Wall -c -o foffer.o foffer.c
gcc -O -Wall -lm -o prover9 prover9.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a
/usr/bin/ld: search.o: in function `search':
search.c:(.text 0x66ef): undefined reference to `round'
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile:66: prover9] Error 1
make[1]: Leaving directory '/home/utente/Downloads/LADR-2009-11A/provers.src'
make: *** [Makefile:7: all] Error 2
I searched and searched, but I am but a humble user. I would be very grateful if somebody could tell me how to solve the error.
CodePudding user response:
This doesn't have anything to do with make. Your code is not safe, and the compiler is warning you about it. Instead of what you have you should be writing:
printf("%s", s2);
etc. If you really don't want to do that, you'll have to specifically disable that warning (by adding -Wall
you've requested all warnings).
Oh, I see you're worried about the error at the end:
search.c:(.text 0x66ef): undefined reference to `round'
that's because your link line is wrong: you've added -lm
at the start of the line. It needs to be at the end; this:
gcc -O -Wall -lm -o prover9 prover9.o ... ../ladr/libladr.a
should instead be:
gcc -O -Wall -o prover9 prover9.o ... ../ladr/libladr.a -lm
Without seeing the makefile rules and variables we can't say how to do this.