Dear Coq discourses,
I am a reasonably competent Coq end-user who is looking to branch out into developing plugins. As part of this process I am looking to move over from writing projects using the Coq makefile approach to the Dune approach. The reason I am trying to move over to the Dune build system now is because in my research it looks like build system has significantly better support for building plugins in ones projects (/ working with Ocaml or other source files in general).
I am not having issues building, at least trivial / test packages using Dune, but I am having / have had problems actually getting to run the finished build in a toplevel, with coqide being my toplevel of choice. I posted a query ragarding this on the proof assistants stack-change and whilst I didn’t receive any help I did find a working solution to get a basic problem working in coqide, which I actually found here on coq-discourse. Please kindly have a look at my question as it adds context to my discussion here without the need for repetition.
Thusfar after finding this solution I have had no issues using Dune for simple projects and feel like I could confidently produce an entire library (sans plugins) using the solution I have found. However pondering the question, it does lead me to a few auxiliary questions that I could do with probing the community with. given below:
-
The solution I found was given in 2019, is this still the intended way to access a Dune-built project in a toplevel or is there a better solution now?
I have seen some debate on this matter here and in git issues, and would love to know the current state of play. -
If the answer to the first question is negative:
Currently the `dummy` _CoqProject file I add to the built dune project (to get the toplevel working) is added to the generated project manually. Obviously this is at best inefficient and at worse unacceptable for a system that is supposed to autobuild an entire project. My knowledge of Dune is limited, is there some stanza I can put in my dune / dune-project file to get dune to automatically copy the _CoqProject from my source files into the built result? Even better, is there some way to get Dune to automatically produce the requisite _CoqProject, as in theory all of the needed information to do so may be extracted from the dune and dune-project files. -
Lastly is a question about getting plugins to work properly in projects built by Dune. Thusfar I have only worked with packages that have been added by the Opam package manager (notably metacoq), which has automatically sorted all of the plumbing information with regards to getting a plugin working with a toplevel. Obviously, when writing my own plugins I will have to sort the logistics out manually. As the dune documentation for building plugins with coq is extensive, I’m sure I will be able to build a package correctly with plugins. My basic question is however, aside from properly referencing a plugins parent package in the _CoqProject - is there anything else logistically that I need to do to ensure that the plugin will work when using it in libraries when in coqide / a toplevel?
As an aside, I think the majority of my confusion is borne out of (incorrectly) assuming that the coq compilation process involved somehow the coq compiler adding some sort of linking information (like relative paths) into the produced .vo/.vok files. That is clearly wrong and perhaps a silly thought to have had in the first place. It looks like now that everything is indeed managed by the _CoqProject / env-variables, but it has left me a bit unsure so I would just like to ask the above questions to sanity check my understanding so I don’t run into any problems further down the line 
.
A second aside related to the first question is that all the coq example dune projects are strictly related to plugins, with only one somewhat pertaining to libraries, and non pertaining to multiple libraries (least not ones with dependencies between them or a _CoqProject as to be inspect-able in a top-level). Whilst there is a skeleton of one in the dune docs I feel like an explicit repo would be really beneficial to on-boarding people onto the Dune build system for coq lest they run into the problems I have been having. I wouldn’t mind quickly writing one up myself but my personal git is not very discoverable to say the least!