[coq] [doc] Some fixes to documentation. #6208
Conversation
|
The directory split advice was the workaround to the META issue that will now be fixed. So it wasn't bogus at some point. |
I think it was bogus back then too. The META issue for me == a missing dependency ; what do you mean by "META issue"? How does splitting into two directories help for a missing dependency to appear? |
|
Note that #6167 still solves nothing, |
doc/coq.rst
Outdated
| - If ``plugins`` is present, Dune will pass the corresponding flags to | ||
| Coq so that ``coqdep`` and ``coqc`` can find the corresponding OCaml | ||
| libraries declared in ``<ocaml_plugins>``. This allows a Coq theory | ||
| to depend on OCaml plugins. Starting with ``(lang coq 0.6)``, |
There was a problem hiding this comment.
I thought we checked for private plugins before 0.6? I may be confused however. I seem to remember introducing the limitation in the workspace composition PR.
There was a problem hiding this comment.
I think that was only checked if the plugins live in a different scope.
With the legacy loading method it is fine to have private libs as plugins, only now that we depend (unconditionally) on the META file this is a hard limitation.
There was a problem hiding this comment.
Private plugins don't make any sense currently in Coq (only for private theories). If you have a public theory then you can install .vo files, however they will rely on the plugin to be installed somewhere to work hence it doesn't make sense to support this.
There was a problem hiding this comment.
Not sure I understand what you mean. Indeed it is logical that private plugins do only make sense for private theories, but that's a valid use case we could support.
There was a problem hiding this comment.
Right I was talking about before. Having private libs in private theories was the only use case that made sense. Private libs in public theories doesn't make any sense. Now with the new loading method however, it means that even private theories can only import public libs which is not currently restricted by Dune IIRC.
To allow for the user case you mention, we would need to yet again change how Coq loads plugins.
There was a problem hiding this comment.
We don't need to change how Coq loads plugins, it is enough for Dune to setup a virtual findlib env where the private libraries are exposed. But that's quite some work tho.
It caused the META file to be build in time by chance. It was only a workaround. |
How did having two directories cause the META file to build? |
|
@ejgallego No idea, that was how we worked around the issue. |
You think you workarounded the issue but I bet you did not, because for Dune that split makes 0 difference, unless I'm missing something. You were likely confused by the terrible (non deterministic) coqdep code. Moreover, now that we correctly setup the findlib env (and META), coqdep outputs garbage, so yeah, the situation was not nice. Maybe a problem was with But if so, that problem still persists no matter what you do with the dirs. Needs to be fixed at the coq lang version level. |
ejgallego
force-pushed
the
coq+doc_fixes
branch
4 times, most recently
from
d62199c to
c2a9c32
Compare
In particular the advice about directory split was bogus. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego
force-pushed
the
coq+doc_fixes
branch
from
c2a9c32 to
153004d
Compare
|
Thanks @christinerose ! |
In particular the advice about directory split was bogus.