search

ejgallego / coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Other
128 stars 39 forks source link

issue when loading mathcomp/HB #260

Closed affeldt-aist closed 2 years ago

affeldt-aist commented 2 years ago

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

ejgallego commented 2 years ago

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.

ejgallego commented 2 years ago

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

affeldt-aist commented 2 years ago

Thank you for the quick answer. At least, this is a clear assessment of the situation.

CohenCyril commented 2 years ago

rebuilding HB without the offending module.

Would that be easy?

ejgallego commented 2 years ago

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.

CohenCyril commented 2 years ago

I'm sorry, I do not understand. CC @gares

gares commented 2 years ago

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...

ejgallego commented 2 years ago

Should be fixed upstream by https://github.com/coq/coq/pull/15220

ejgallego commented 2 years ago

Closed by https://github.com/ocaml/opam-repository/pull/22087