Stream: Coq devs & plugin devs

Topic: Spurious failure with primitive floats and native compile

view this post on Zulip Gaëtan Gilbert (May 11 2020 at 19:23):

Interesting(?) spurious(?) failure in https://gitlab.com/coq/coq/-/jobs/545904250 (test-suite:edge+flambda)

File "./primitive/float/compare.v", line 324, characters 0-50:
Error:
Dynlink error: The module `Coq_native6feb64' is already loaded (either by the main program or a previously-dynlinked library)

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2020 at 22:51):

@Gaëtan Gilbert this may not seem spurious, maybe the linker is violating the >= 4.08 invariant about doubly-linking modules?

view this post on Zulip Gaëtan Gilbert (May 12 2020 at 09:26):

I mean spurious in the sense that it's not caused by the specific PR it was run for

view this post on Zulip Maxime Dénès (May 13 2020 at 09:17):

Is there an open issue?

Last updated: Apr 19 2024 at 02:02 UTC