Louise Dubois de Prisque (Apr 13 2023 at 13:38): Louise Dubois de Prisque (Apr 13 2023 at 13:38):Hello ! While loading a Coq plugin (coq-actema) and loading elpi at the same time, I encountered this error message:
Dynlink error: The module `Re__' is already loaded (either by the main program or a previously-dynlinked library)
Have you any idea of where it comes from? I use coq-8.15.2 and for compatibility reasons I cannot use another version for now.
Enrico Tassi (Apr 13 2023 at 14:28):I guess coq-actema uses re as well as elpi (hence coq-elpi).
This error became fatal after OCaml 4.07.
In more recent versions of Coq we solve the problem by using findlib, which avoids loading the same version of an ocaml module.
If you cannot update Coq, you could try to use OCaml 4.07.
Hope it helps.
Louise Dubois de Prisque (Apr 13 2023 at 14:51):Thank you Enrico ! Do you know if this error is solved in Coq-8.16 or only in 8.17?
Enrico Tassi (Apr 13 2023 at 16:23):I believe 8.16, but maybe one needs to patch coq-actema to use the new loading mechanism (Elpi is fine).
Last updated: Oct 13 2024 at 01:02 UTC