coq-serapi
coq-serapi copied to clipboard
ejgallego
issue when loading mathcomp/HB
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.")
See https://github.com/cpitclaudel/alectryon/issues/71
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:
- https://github.com/coq/coq/issues/12067
- https://github.com/coq/coq/issues/7698
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.
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.
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...
