CompCert doesn't seem to compile with the last version of Menhir

[giltho]

Hello !

CompCert is not compiling properly with the last version of Menhir.

Here's the configuration :

Testing assembler support for CFI directives... yes
    Testing Coq... version 8.10.2 -- good!
    Testing OCaml... version 4.08.1 -- good!
    Testing OCaml .opt compilers... yes
    Testing Menhir... version 20200123 -- good!
    Testing GNU make... version 3.81 (command 'make') -- good!
    
    CompCert configuration:
        Target architecture........... x86
        Hardware model................ 64
        Application binary interface.. macosx
        Endianness.................... little
        OS and development env........ macosx
        C compiler.................... gcc -arch x86_64
        C preprocessor................ gcc
        Assembler..................... gcc
        Assembler supports CFI........ true
        Assembler for runtime lib..... gcc -arch x86_64 -c
        Linker........................ gcc
        Linker needs '-no-pie'........ false
        Math library.................. 
        Build command to use.......... make
        Binaries installed in......... /usr/local/bin
        Runtime library provided...... true
        Library files installed in.... /usr/local/lib/compcert
        Standard headers provided..... true
        Standard headers installed in. /usr/local/lib/compcert/include
        Coq development will not be installed

With these parameters, it seems that CompCert is not building, using :

./configure x86_64-macosx #as showed above
make -j 4

The compilation dies in the middle. Here are the last few lines :

...
OCAMLOPT extraction/Memtype.ml
    OCAMLOPT extraction/PeanoNat.ml
    OCAMLOPT cparser/Machine.ml
    OCAMLC   cparser/Env.mli
    OCAMLC   cparser/Cprint.mli
    OCAMLOPT extraction/Ring.ml
    OCAMLOPT lib/Printlines.ml
    OCAMLOPT extraction/DecidableClass.ml
    OCAMLC   cparser/Transform.mli
    OCAMLOPT extraction/Cabs.ml
    OCAMLOPT cparser/pre_parser_aux.ml
    OCAMLC   cparser/pre_parser.mli
    OCAMLC   cparser/Cflow.mli
    File "cparser/pre_parser.mli", line 114, characters 10-56:
    114 |   include MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    Error: Unbound module MenhirLib
    make[2]: *** [cparser/pre_parser.cmi] Error 2
    make[2]: *** Waiting for unfinished jobs....
    make[1]: *** [ccomp] Error 2
    make: *** [all] Error 2

However, everything seems to be fine using Menhir 20190924.
You may have already noticed this issue, but given that the menhir version that causes the issue was released 2 days ago I thought I'd notify you :)

[xavierleroy]

Thanks for the early notice. We're investigating.

[jhjourdan]

@fpottier, you may want to have a look to that.

[bschommer]

In this case you are just missing the menhirLib (which is now a separate package in opam). However with the most recent version of menhir this still won't work, since the menhirLib no longer contains the necessary menhirLib.o file in order to link. So it is best to stay at the older version at the moment.

[xavierleroy]

The CompCert sources include a copy of menhirLib, so it's not just a case of a missing external library.

[bschommer]

The CompCert sources include a copy of menhirLib, so it's not just a case of a missing external library.

The coq version, but not the OCaml version, which is needed for the error message handling of the pre_parser.

[fpottier]

Hello! menhirLib.o is no longer installed; only menhirLib.a is installed. It seems that the problem was in Makefile.menhir where menhirLib.cmx was mentioned (for some reason) whereas menhirLib.cmxa should have been mentioned instead. I have made a pull request with this fix.