Stream: Coq devs & plugin devs

Topic: Dynlink module already loaded


view this post on Zulip Jason Gross (Nov 29 2021 at 18:24):

What does the following error mean?

Error: Dynlink error: The module `Coq_native13c5a0' is already loaded (either by the main program or a previously-dynlinked library)

https://github.com/coq-community/coq-performance-tests/runs/3479329691?check_suite_focus=true#step:6:754

view this post on Zulip Jason Gross (Nov 29 2021 at 18:38):

Would backtracking across native_compute result in an error like this?

view this post on Zulip Gaƫtan Gilbert (Nov 29 2021 at 18:39):

perhaps it generated the same file name twice
it's generating file names using a random suffix (the 13c5a0 part) to get a not-already-used name, but since it deletes the file after using it collisions are still possible

view this post on Zulip Jason Gross (Nov 29 2021 at 19:07):

Reported as https://github.com/coq/coq/issues/15263


Last updated: Feb 06 2023 at 20:02 UTC