Is there some way CI can check for module name clashes between Coq and a plugin? As one example, the recent creation of
stm/partac.ml caused a clash with CoqHammer: https://github.com/lukaszcz/coqhammer/issues/89
I would guess we could avoid this someday by properly packaging all of Coq's modules under a Coq namespace, no?
I thought the Dune Coq build will be / is wrapped, i.e., no
(wrapped false)? I think this would solve the issue from Coq's side. However, as long as
make builds of Coq are allowed and plugins don't use proper wrapping, I guess clashes will be possible.
anyway, we managed to make CoqHammer builds fully wrapped both with
make and Dune now.
we're not wrapping as long as we keep the make path around afaik
what is the plan for Dune builds becoming default? 8.14-ish or earlier?
The plan has already been ASAP. But it has been delayed on some features not being supported (in particular native).
I did put an item for the CUDW, it may be a good occasion to "sprint"
Last updated: May 31 2023 at 15:01 UTC