在Ubuntu上安装CompCert C编译器时出现问题



我正在按照此处的说明安装CompCert C编译器:https://compcert.org/man/manual002.html.

然而,我被困在这样一个阶段:;使用适当的选项运行配置脚本:/配置[选项…]目标";

控制台输出为:

~/compcert/CompCert-3.8$ ./configure -use-external-MenhirLib x86_64-linux
Testing assembler support for CFI directives... yes
Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie'
Testing Coq... version 8.11.0 -- good!
Testing OCaml... version 4.08.1 -- good!
Testing OCaml native-code compiler...yes
Testing OCaml .opt compilers... yes
Testing Menhir... version 20200123 -- good!
Error: cannot determine the location of the Menhir API library.
This can be due to an incorrect Menhir package.
Consider using the OPAM package for Menhir.
Testing GNU make... version 4.2.1 (command 'make') -- good!
One or several required tools are missing or too old.  Aborting.

我运行的是Ubuntu 20.04 LTS。

[编辑:我成功地运行了./configure。但是我无法重现我的确切方法。现在我陷入了另一个部分。]

后续问题:

运行make all时,我收到以下输出:

/compcert/CompCert-3.8$ make all
make proof
make[1]: Entering directory '/home/user/compcert/CompCert-3.8'
COQC Axioms.v
Error: Can't find file ./Axioms.v
make[1]: *** [Makefile:226: Axioms.vo] Error 1
make[1]: Leaving directory '/home/user/compcert/CompCert-3.8'
make: *** [Makefile:155: all] Error 2

我通过将lib/Axiom.v复制到根目录来解决这个问题。然后make all抱怨lib/中的另一个库,所以我移动了一堆,直到收到以下错误:

~/compcert/CompCert-3.8$ make all
make proof
make[1]: Entering directory '/home/user/compcert/CompCert-3.8'
COQC Ordered.v
File "./Ordered.v", line 90, characters 16-19:
Error: The reference int was not found in the current environment.
make[1]: *** [Makefile:226: Ordered.vo] Error 1
make[1]: Leaving directory '/home/user/compcert/CompCert-3.8'
make: *** [Makefile:155: all] Error 2

现在我又陷入了困境。

您的menhirLib版本似乎不正确。请参阅生成系统中configure脚本中导致此错误的这些行。我认为问题是您安装了不同版本的menhirLib,可能是使用了您的包管理器。

我建议您运行以下命令从opam安装最新的menhirLib

opam update
opam install menhir menhirLib

这应该会有所帮助。

最新更新