Alt-ergo incompatible with menhir.20211125 when using ocaml 4.08, 4.09 or 4.10 ?

[fblanqui]

Hi. I have a strange error this morning. See https://github.com/Deducteam/lambdapi/runs/4332121191?check_suite_focus=true. Alt-ergo fails when menhir is upgraded from 20211012 to 20211125 but opam info menhir mentions no 20211125 version for menhir on my machine...

[Stevendeo]

It is very strange that it works with OCaml 4.11 but not in OCaml 4.10.2 (at least according to your CI). I am checking that it is also the case locally, but it might be (somehow) a bug on menhir's side.

[fblanqui]

Concerning menhir 20211125, I now see it on my machine with opam info.

[Stevendeo]

You're right I just noticed it too. For now I suggest you use the previous version of menhir. My understanding is that the OCaml typer has been fixed in 4.11.0 to accept some tricky quantified types, and menhir now generates such types.

[fblanqui]

I added an issue on menhir: https://gitlab.inria.fr/fpottier/menhir/-/issues/57.

[Stevendeo]

If the issue is solved, I will close it