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)
Would backtracking across native_compute
result in an error like this?
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
Reported as https://github.com/coq/coq/issues/15263
Last updated: Oct 13 2024 at 01:02 UTC