Trouble Installing CompCert C compiler on Ubuntu

Question

I'm installing CompCert C compiler as instructed here: https://compcert.org/man/manual002.html.

However I'm stuck at the stage where I "Run the configure script with appropriate options: ./configure [option …] target "

The console output is:

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

I'm running Ubuntu 20.04 LTS.

[Edit: I managed to run the ./configure. However I cannot reproduce the exact method how I did it. Now I'm stuck in a different part.]

Follow-up question:

When running make all I receive the following output:

/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

I fixed that problem by copying lib/Axiom.v to the root. The make all then complained about another library in lib/ so I moved a bunch of them until I received the following error:

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

And now I'm stuck once again.

Answer 1

It seems that you have an incorrect version of the menhirLib. See these lines in the configure script in the build system which lead to this error. I think the problem is that you installed a different version of menhirLib, possibly using your package manager.

I suggest you to run the following commands to install the latest menhirLib from the opam:

opam update
opam install menhir menhirLib

This should help.