After learning to write libraries for Coq using the Makefile approach I have decided to take the plunge and try to switch over to using the Dune system. My question consists of help with getting to grips with the practicalities of using this build system, in particular actually working with the project once it has been built by Dune.
Context
For context I have a little experience with Ocaml but I only ever manually compiled my code / wrote up a little make-file, so I am a complete novice when it comes to using Dune. Thankfully the Dune Docs have a pretty comprehensive beginners guide for coq-projects which I have managed to create a simple test repo that is based on their Multi-Theory Project example. It contains two sub-directories A and B directly below the dune root each with their respective coq-files a.v and b.v plus individual dune files, all given as follows:
A/a.v
Definition A := 1.
Definition B := 2.
A/dune
(include_subdirs qualified)
(coq.theory
(name A))
B/b.v
From A Require Import a.
Print A.
B/dune
(coq.theory
(name B)
(theories A))
dune-project
(coq.theory
(name B)
(theories A))
Running dune build at the root proceeds to build the project without a hitch and produces the output below:
A = 1
: nat
I believe this shows that dune is working correctly as in the building stage it is running the Print A command in b.v. Note that running dune build again produces no output, I presume because there are no changes and so dune recognizes this.
All seems well and good thusfar.
In my previous Coq workflow I simply (once my _CoqProject is set up), make my project, launch up coqide and then edit it by stepping through it in the IDE and making changes as I go. when I'm done / need to rebuild a dependency I simply clean and make again and it just works after re-launching coqide.
I naively tried doing this with the Dune project above (after building launching coqide on the .v files in the _build/default directory and it does not work. Notable on the first line of b.v it errors out with the usual error when it cant find a load-path.
I looked on further in the dune tutorial on Running a toplevel on a Dune Project. I surmise that it is exactly what I'm looking for, that is manually inspecting the built files in a top-level (coqide). It tells me to run the command:
dune coq top <file> --toplevel=coqide
to view the files in IDE but I am having trouble getting it to work. Noteably here are the commands I have tried (being run from my terminal at the Dune root):
>dune coq top _build/default/B/b --toplevel=coqide
Error: Cannot find file: _build/default/B/b
Hint: Is the file part of a stanza?
Hint: Has the file been written to disk
I'm not exactly sure about the first hint (about stanzas), as b.v should be part of the coq.theory B. and for the latter yes all my files have been written to disk!
Secondly I tried simply calling:
>dune coq top B/b.v --toplevel=coqide
In this case I get no error and coqide launches. However it launches as if I had just called it normally - i.e. just opening a blank *Scratch* file, so this seemingly does not work either.
At this point I don't really know how to proceed.
Question
How does one go about interactively viewing the coq project/library that has just been built by Dune in coqide?
I have the feeling that I'm just making a small silly mistake either with my understanding of Dune or with typing in a command, however try as I might I can't get the thing to work. Whilst I could go back to using the make-file approach from my research it looks like Dune has much better support for building things like Coq-plugins, which I'd like to get stuck into at some point down the road. Thusly I would apprentice someone with more knowledge of using the Dune build with coq system having a look at my problem!
