ubuntu - 安装prover9时使所有命令返回错误

Question

我正在尝试在 Ubuntu 20.10 上安装自动定理证明器 prover9。于是我去了this page并下载文件“LADR-2009-11A.tar.gz”。然后，我按照 this page 上的说明进行操作。并执行了这些行

zcat LADR-2009-11A.tar.gz | tar xvf -
cd LADR-2009-11A
make all

不幸的是，第三行导致错误:“undefined reference to round”(我认为)。
完整的输出消息在这里:

     ~/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

我找了又找，但我只是一个不起眼的用户。如果有人能告诉我如何解决该错误，我将不胜感激。

Answer 1

这与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 规则和变量，我们不能说如何做到这一点。