Блог

Я устанавливаю компилятор 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
 

И теперь я снова застрял.

Похоже, у вас неправильная версия menhirLib. Посмотрите эти строки в configure скрипте в системе сборки, которые приводят к этой ошибке. Я думаю, проблема в том, что вы установили другую версию menhirLib , возможно, с помощью вашего менеджера пакетов.

Я предлагаю вам выполнить следующие команды для установки последней menhirLib версии из opam:

 opam update
opam install menhir menhirLib
 

Это должно помочь.