Stream: Coq devs & plugin devs

Topic: Coq/plugin module name clashes


view this post on Zulip Karl Palmskog (Oct 11 2020 at 12:26):

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

view this post on Zulip Matthieu Sozeau (Oct 13 2020 at 16:00):

I would guess we could avoid this someday by properly packaging all of Coq's modules under a Coq namespace, no?

view this post on Zulip Karl Palmskog (Oct 13 2020 at 16:03):

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.

view this post on Zulip Karl Palmskog (Oct 13 2020 at 16:05):

anyway, we managed to make CoqHammer builds fully wrapped both with make and Dune now.

view this post on Zulip Gaëtan Gilbert (Oct 13 2020 at 16:38):

we're not wrapping as long as we keep the make path around afaik

view this post on Zulip Karl Palmskog (Oct 13 2020 at 16:59):

what is the plan for Dune builds becoming default? 8.14-ish or earlier?

view this post on Zulip Théo Zimmermann (Oct 13 2020 at 18:06):

The plan has already been ASAP. But it has been delayed on some features not being supported (in particular native).

view this post on Zulip Enrico Tassi (Oct 13 2020 at 18:07):

I did put an item for the CUDW, it may be a good occasion to "sprint"


Last updated: Oct 15 2021 at 20:02 UTC