Stream: Coq devs & plugin devs

Topic: native compiler errors


view this post on Zulip Jason Gross (May 27 2021 at 22:08):

I'm getting a lot of error messages from the native compiler, nondeterministically, on CI minimization. Things like

File "/tmp/.coq-native/Ntmppzzwwkvv.native", line 59, characters 2-61:
59 |   NInterval_Float_Basic.indaccu_NInterval_Float_Basic_float_0
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module NInterval_Float_Basic
Error: Native compiler exited with status 2

What's up with these error messages?

view this post on Zulip Jason Gross (May 27 2021 at 22:10):

cf https://github.com/coq-community/run-coq-bug-minimizer/runs/2689270840?check_suite_focus=true#step:5:55571

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2021 at 00:11):

Wild guess but maybe https://github.com/coq/coq/issues/13035 ?


Last updated: Oct 16 2021 at 02:03 UTC