Impossible to build Why3 due to `parser/handcrafted.messages`
Ocamlopt src/util/mlmpfr_wrapper.ml
File "src/util/mlmpfr_wrapper.ml", line 1:
Error: Could not find the .cmi file for interface
src/util/mlmpfr_wrapper.mli.
Makefile:2244: recipe for target 'src/util/mlmpfr_wrapper.cmx' failed
And this is caused by parser/handcrafted.messages
!
More precisely, my version of menhir
produces a slightly different file parser/handcrafted.messages.temp
(semantically identical, but not byte-to-byte). As a consequence, the generation of src/parser/parser_messages.ml
fails. But since it fails at dependency generation time, the error is ignored, dependency generation is aborted, and the actual build starts. The build eventually fails because .dep
files were not properly generated due to the above failure.
So, not only the user is unable to build Why3, but the build error message is completely misleading. (I wasted quite some time trying to understand what was wrong with mlmpfr_wrapper.ml
.)
@bobot @sdailler If we can't find a solution by 1.3.0, I will again revert this code.