Feature: better support for dune

[lgaeher]

For Coq projects using dune instead of coq-makefile, currently still a dummy _CoqProject file is required for use with Coqtail (that points Coq to the right path to search for dune build artifacts, i.e. other .vo files). This works more or less well, depending on the project topology. A better way would be to use dune's support for running a coqtop instance with the right configuration (https://dune.readthedocs.io/en/stable/coq.html#running-a-coq-toplevel).

Some initial considerations have been made for other Coq interfaces (e.g. https://github.com/ProofGeneral/PG/issues/477#issuecomment-1145349170) , but to my knowledge none of them currently implements good support for dune.

[whonore]

From the docs you linked, it seems like it should mostly be a matter of calling dune coq top --toplevel=coqidetop instead of coqidetop, but so far I haven't gotten that to work. I've never used dune for a Coq project though so I may be setting it up wrong. I'll read the docs more carefully and keep trying. In the meantime, if you or anyone else feels like experimenting with this, it might be possible to get something working through some combination of g:coqtail_coq_prog and passing arguments to CoqStart.

[lgaeher]

Thanks! I have some time in the next few days and will try to experiment a bit with this

[lgaeher]

I've gotten something to work using dune coq top [filename] --toplevel echo that seems to work pretty well in my tests so far: https://github.com/whonore/Coqtail/compare/main...lgaeher:Coqtail:better-dune-support

The problem with using dune coq top to launch coqtop directly is that it always expects a filename for which dune can analyze the dependencies. So that doesn't work for launching Coqtail in a buffer that hasn't been saved yet.

With --toplevel echo, we can get all the options we would pass in the case that there's a filename provided, and then pass these arguments to the existing launch interface.

Caveats currently:

• this blocks when dune needs to compile dependencies. Potentially we could make calling start non-blocking?
• if you create a new unsaved buffer with dependencies from your current project, you will have to save first before starting Coqtail, as otherwise it won't find the dependencies. (this is something which works when using _CoqProject, I think, but isn't a very common occurrence)
• this should have better error reporting. E.g. report that this is a dune project, but dune does not know how to build the file, etc.

[lgaeher]

It would also be good to fix GoToDef and the taglist to refer to the source files and not dune's copy in the build directory. We could do something like this https://github.com/cpitclaudel/company-coq/pull/257, stripping _build/default/ in the path to the source. I found the place where the taglist and quickfix list get populated in the Coqtail sources, and tried to make the change -- not sure if this is the best way to do it, since I don't understand vimscript much: https://github.com/whonore/Coqtail/commit/5daa7f4b121bb33f4cce59de2507d03d2cdaf264, but in my brief test it seems to work as intended