1

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.

Keyboard_Crasher
  • 55
  • 8

1 Answers1

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.

jubnzv
  • 1,526
  • 2
  • 8
  • 20
  • I receive the this output when following the instructions: `$ opam install menhir menhirLib [NOTE] Package menhirLib is already installed (current version is 20210310). [NOTE] Package menhir is already installed (current version is 20210310).` The install instructions say is should have "The Menhir parser generator, version 20190626 or newer". [Edit. Please pardon me for missing the newlines in the code block] – Keyboard_Crasher Mar 18 '21 at 15:10
  • @Keyboard_Crasher Aha, it seems that you have installed a different ocaml version in your system. From your original post, you have Menhir version `20200123`, but `opam install` says that the current version is `20210310`. – jubnzv Mar 18 '21 at 18:33
  • Can you show the output of `opam switch list` command? – jubnzv Mar 18 '21 at 18:34
  • `opam switch list` only shows that my version of Ocaml is 4.08.1. However I'm now able to run `./configure` without errors. Thanks you for your help. – Keyboard_Crasher Mar 18 '21 at 19:41