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: Oct 13 2024 at 01:02 UTC