我试图在Ubuntu20.10上安装自动定理证明程序prover9。于是我去了此页,下载了文件"LADR-2009-11A.tar.gz“。然后,我按照此页上的说明执行了以下几行
zcat LADR-2009-11A.tar.gz | tar xvf -
cd LADR-2009-11A
make all
不幸的是,第三行导致了一个错误:“对圆的未定义引用”(我认为)。
完整的输出消息如下:
~/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
我到处寻找,但我只是一个谦逊的用户。如果有人能告诉我如何解决这个错误,我将非常感激。
发布于 2021-12-17 15:53:55
这和make无关。您的代码不安全,编译器正在警告您。而不是你拥有的东西,你应该写:
printf("%s", s2);
等等,如果你真的不想这样做,你必须特别禁用这个警告(通过添加-Wall
你请求了所有的警告)。
哦,我看到你担心最后的错误:
search.c:(.text+0x66ef): undefined reference to `round'
这是因为您的链接行是错误的:您已经在行的开头添加了-lm
。它必须在最后;这是:
gcc -O -Wall -lm -o prover9 prover9.o ... ../ladr/libladr.a
相反,应:
gcc -O -Wall -o prover9 prover9.o ... ../ladr/libladr.a -lm
如果没有看到makefile规则和变量,我们就无法说明如何做到这一点。
https://stackoverflow.com/questions/70388065
复制相似问题