issue when loading mathcomp/HB
affeldt-aist opened this issue · 9 comments
Hi,
I am just forwarding an issue identified @Zimmi48
that I seem to have run into when testing alectryon.
It seems to be an issue that arises by just loading modules as in
(Add () "From mathcomp Require Import all_ssreflect.")
(Add () "From HB Require Import structures.")
Hi @affeldt-aist , thanks for the report.
This is a big problem indeed, it is due to the HB plugin using -linkall, which has been forbidden since OCaml 4.08 . As sercomp already includes the result module, OCaml's dynamic linker refuses to doubly-link the module.
The solution is not easy, other than rebuilding HB without the offending module.
Another solution is to use OCaml <= 4.07 , or add result to the list of forbidden modules in CoqMakefile.
Relevant Coq issues are:
This is going to get worse and worse I'm afraid :S
Thank you for the quick answer. At least, this is a clear assessment of the situation.
rebuilding HB without the offending module.
Would that be easy?
Would that be easy?
That's easy, as CoqMakefile already has a list of "forbidden" modules.
However, you get a different problem, and it is that now Coq will fail to Dynload HB as it doesn't link the result module :S
The proper solution is to implement dependencies on Coq's linker, as outlined above, but that's not trivial. I'm much afraid that it is not possible to have sertop and coqc link to the same exact set of modules.
The only reliable workaround is to stay in 4.07 . While we got bitten by this problem here, you will get the problem with coqtop too the moment you load two plugins that happen to refer the same module.
I'm sorry, I do not understand.
CC @gares
the problem is that elpi links ppx stuff, which is also linked by serapi.
Use 4.07 for generating the doc :-/ which tolerates double linking of the same module.
We will eventually fix the issue in Coq...
Should be fixed upstream by coq/coq#15220
Closed by ocaml/opam-repository#22087