0

我正在按照此处的说明安装 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

现在我又被困住了。

4

1 回答 1

0

看来您的menhirLib版本不正确。在构建系统的脚本中查看导致此错误的这些行。configure我认为问题在于您安装了不同版本的menhirLib,可能使用了您的包管理器。

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

opam update
opam install menhir menhirLib

这应该会有所帮助。

于 2021-03-18T13:42:20.660 回答