首页
学习
活动
专区
圈层
工具
发布
首页
学习
活动
专区
圈层
工具
MCP广场
社区首页 >问答首页 >在安装prover9时使所有命令返回错误

在安装prover9时使所有命令返回错误
EN

Stack Overflow用户
提问于 2021-12-17 03:24:57
回答 1查看 75关注 0票数 0

我试图在Ubuntu20.10上安装自动定理证明程序prover9。于是我去了此页,下载了文件"LADR-2009-11A.tar.gz“。然后,我按照此页上的说明执行了以下几行

代码语言:javascript
运行
复制
zcat LADR-2009-11A.tar.gz | tar xvf -
cd LADR-2009-11A
make all

不幸的是,第三行导致了一个错误:“对圆的未定义引用”(我认为)。

完整的输出消息如下:

代码语言:javascript
运行
复制
     ~/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

我到处寻找,但我只是一个谦逊的用户。如果有人能告诉我如何解决这个错误,我将非常感激。

EN

Stack Overflow用户

回答已采纳

发布于 2021-12-17 15:53:55

这和make无关。您的代码不安全,编译器正在警告您。而不是你拥有的东西,你应该写:

代码语言:javascript
运行
复制
printf("%s", s2);

等等,如果你真的不想这样做,你必须特别禁用这个警告(通过添加-Wall你请求了所有的警告)。

哦,我看到你担心最后的错误:

代码语言:javascript
运行
复制
search.c:(.text+0x66ef): undefined reference to `round'

这是因为您的链接行是错误的:您已经在行的开头添加了-lm。它必须在最后;这是:

代码语言:javascript
运行
复制
gcc  -O -Wall -lm -o prover9 prover9.o ... ../ladr/libladr.a

相反,应:

代码语言:javascript
运行
复制
gcc  -O -Wall -o prover9 prover9.o ... ../ladr/libladr.a -lm

如果没有看到makefile规则和变量,我们就无法说明如何做到这一点。

票数 0
EN
查看全部 1 条回答
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/70388065

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档