metacoq/translations/times_bool_fun2.v is incompatible with the native compiler (Anomaly "Uncaught exception UGraph.UniverseInconsistency(_).")

Open JasonGross opened this issue 3 years ago • 2 comments

With Coq 8.16.0, Equations tag v1.3-8.16, metacoq at the tip of coq-8.16 (d702f18ce289530cdd0be3d0ad331cb1ad38f6a0), when coq-native has been installed, the build fails with

COQNATIVE times_bool_fun2.vo
Error: Anomaly "Uncaught exception UGraph.UniverseInconsistency(_)."
       Please report at http://coq.inria.fr/bugs/.
make[3]: *** [Makefile.coq:795: times_bool_fun2.vo] Error 129
make[3]: *** Deleting file 'times_bool_fun2.vo'

(after manually bypassing the native compiler to get around https://github.com/MetaCoq/metacoq/issues/771)

Oct 13 '22 08:10 JasonGross

Isn't this https://github.com/coq/coq/issues/16599?

Oct 13 '22 08:10 ppedrot

Ah, looks very plausibly like that

Oct 13 '22 08:10 JasonGross