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

Question

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

然而，我仍然停留在“使用适当的选项运行配置脚本：./configure option…target”的阶段。

控制台输出为：

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

现在我又被卡住了。

Answer 1

您的menhirLib版本似乎不正确。请参阅导致此错误的构建系统中configure脚本中的these lines。我认为问题在于您安装了不同版本的menhirLib，可能是使用您的包管理器。

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

opam update
opam install menhir menhirLib

这应该会有帮助。