Programs like compcert (https://compcert.org/compcert-C.html) say they require "the Menhir parser generator, version 20190626 or newer" (see section 2.2.1 of https://compcert.org/man/manual002.html#install), so one is led to believe that by installing, say, menhir 20211012 this prerequisite would be fullfilled. However, the above is only partially true. compcert, for example, does not only require strictly menhir (the parser generator), but also a library that is installed in the user-contrib directory (indicating, to me at least, a third-party, optional, "user-contributed" library): coq-menhirlib. To a beginner, like me, the naming of the library is very unfortunate (even if it bears some logic): I was *sure* that, by having installed coq and menhir (which installs a "menhirLib" already), I was done. I was not. For one, menhirLib and coq-menhirlib are two different things. For another, and that's the purpose of this bug report, the menhir ebuild does not install coq-menhirlib, even though everything is there, as far as the sources are concerened: coq-menhirlib is part of the menhib tarball. Thus, I was very surprised to see compcert compilation fail with COQC cparser/Parser.v File "./cparser/Parser.v", line 11, characters 0-28: Error: Cannot find a physical path bound to logical path Main with prefix MenhirLib. make[1]: *** [Makefile:257: cparser/Parser.vo] Error 1 make[1]: Leaving directory '/usr/src/compcert-3.12' make: *** [Makefile:181: all] Error 2 when instructed to use the "external" (presumably already installed) "MenhirLib" (mind the capital M) with ./configure -use-external-Flocq -use-external-MenhirLib -clightgen x86_64-linux Filing a bug report (https://github.com/AbsInt/CompCert/issues/469) did not bring up anything constructive, besides the fact that the compcert developer will "not going to help you debug the packages from your distribution" (good to know, for you too...) and the hint that all what is needed are the "coq, menhir, coq-flocq and coq-menhirlib OPAM packages". As I said, I am new to all this, so I had to find out what is actually missing (answer: coq-menhirlib, not to be confused with either coq, or menhirlib), find out where to get it from (answer: the menhir sources themselves), look into the ebuild and find a way to install what is missing (see below). The painful path to enlightment The remark that I should be using OPAM and that the packages are "coq, menhir, coq-flocq and coq-menhirlib" made me eventually think that "menhirlib" and "coq-menhirlib" may be two different packages indeed. Looking at the source code of menhir, precisely in dune-project I could see that there was indeed a coq-menhirlib dune package defined: (package (name coq-menhirlib) ) Adding just dune_src_install coq-menhirlib to the other "dune_src_install ..." commands of the ebuild, however, did NOT make any difference, except for the installation of the two files: /usr/lib64/ocaml/coq-menhirlib/dune-package /usr/lib64/ocaml/coq-menhirlib/META Clearly, more was needed. Finally, I got my inspiration from the .spec file of the source RPM https://download-ib01.fedoraproject.org/pub/fedora/linux/releases/37/Everything/source/tree/Packages/o/ocaml-menhir-20220210-9.fc37.src.rpm of the Fedora coq-menhirlib-20220210-9.fc37.x86_64 package: https://fedora.pkgs.org/37/fedora-x86_64/coq-menhirlib-20220210-9.fc37.x86_64.rpm.html and crafted a solution: Solution Modify the menhir-20211012 ebuild to also install "coq-menhirlib", by adding (quick'n dirty!): make -C coq-menhirlib make -C coq-menhirlib install DESTDIR=${D} dune_src_install coq-menhirlib to src_install()... To me, it looks somewhat "quick'n dirty" to put a compilation instruction make -C coq-menhirlib in src_install() - but it works this way, while it did not work when I put it into an extra src_compile()... FYI the above compiles and installs --- /usr/lib64/coq/user-contrib/ --- /usr/lib64/coq/user-contrib/MenhirLib/ >>> /usr/lib64/coq/user-contrib/MenhirLib/Automaton.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter_correct.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Version.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter_complete.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter_complete.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_safe.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_complete.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter_correct.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Grammar.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Main.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_complete.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_complete.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter_complete.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Version.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Alphabet.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Main.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Grammar.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Alphabet.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Automaton.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Main.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter_correct.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_classes.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_safe.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Version.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_safe.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Interpreter.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Alphabet.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_classes.vo >>> /usr/lib64/coq/user-contrib/MenhirLib/Validator_classes.v >>> /usr/lib64/coq/user-contrib/MenhirLib/Automaton.glob >>> /usr/lib64/coq/user-contrib/MenhirLib/Grammar.vo which are the "external MenhiLib" files needed by programs like compcert. Please incorporate this change into the menhir ebuild. Of course, you will probably need to introduce a new USE flag ('coq'?) and enclose the above three lines inside a check (if use coq...). Or create an extra package, say, coq-menhirlib that compiles and installs the coq-menhirlib part of the menhir sources. I am sure there are established procedures on which way to choose here. Now, bear with me while I will be formatting the above, in a second, editing step... :-)
Oops..I can't find a way to edit an already posted comment of mine - too accustomed to GitHub I guess... :-) You have to be content with the unformatted report, sorry...
https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d9fe66b2052fae9473fa7abc1a00b338b63d8e00
WOW! What a Christmas present! THANK YOU! :-) Happy Holidays and best wishes for a happy and peaceful New Year!
Merry Christmas to you too segmentation fault, hope the install image is sufficient.
