Support dune builds

[Blaisorblade]

When using dune, currently VsCoq won't be able to find and load built .vo files (ditto ProofGeneral/CoqIDE).
This is a known problem, but I'm filing this issue as documentation and to post the current workaround.
I'm using an issue as documentation on purpose, since this is still pretty hacky.

As confirmed by @ejgallego, the workaround is to modify _CoqProject as follows:

--Q theories D
+-Q _build/default/theories D

Beware this breaks tasks that use coq_makefile, but I expect on *nix one can try processing _CoqProject with sed -e 's!_build/default/!! before passing it to coq_makefile.

[gares]

Thanks for posting. I guess the plan is to invoke coq*top via dune, since only dune knows the actual profile (which may not be default). In the meanwhile this is better than nothing ;-)

[k4rtik]

It seems there is some movement to improve dune support in PG via company-coq, see cpitclaudel/company-coq#257

Is there any progress in VSCoq?

[Blaisorblade]

Haven’t heard anything, and that MR seems about jump-to-definition only, which is unsupported altogether in vscoq.

[fakusb]

Probably one would just need to detect if the current project is a dune-project, and prepend something to the command line arguments of coqtop that tell where to look for the libraries. And one probably want to have an option in vscode to force either of he two ways instead of the auto-detection.

I have never used dune. Can someone link a small project with the default setup for a dune-coq-project?

[k4rtik]

@fakusb thanks for taking a look, here's a template project: https://github.com/palmskog/coq-program-verification-template

Especially notice the caveat at https://github.com/palmskog/coq-program-verification-template#caveats We are looking to improve this situation from VSCoq perspective, so one can imagine being able to work on this project with VSCoq when the Makefile* and _CoqProject are deleted.

Currently, a suboptimal hack mentioned above in the OP is required.

[gares]

See also #361

[Zeta611]

Is there an update on this? The workaround

-Q _build/default/theories D

still works, but it took quite some time to find this issue page for the workaround. Or can we document this somewhere to make it more discoverable?

[gares]

This is still TODO.
The correct solution would be to depend on dune-rpc and use this API:
https://github.com/ocaml/dune/blob/6152ab8ec5d7204d792be7b094063c032bfdd3cc/otherlibs/dune-rpc/dune_rpc.mli#L334