Hello. I followed Plugin examples in the repo and this tutorial and setup the plugin development toolchain
The current situation is I have two building procedure, one using makefile (coqproject/coq-makefile?) and the other using dune. I use makefile style to test the plugin (interactively inside VSCoq) and I use dune so that my vscode-ocamllsp can react correctly. I haven't even setup the proper debugging feature (those fancy step-wise debugging form) and only use print statement to debug the plugin inside Coq.
There is a plugin example in the Dune docs too: https://dune.readthedocs.io/en/stable/coq.html#coq-plugin-project
Using both coq_makefile and Dune will be tricky. You should be able to do everything with Dune.
Ali Caglayan said:
Using both coq_makefile and Dune will be tricky. You should be able to do everything with Dune.
I see in section https://dune.readthedocs.io/en/stable/coq.html#running-a-coq-toplevel here dune can only interact with coqtop? Is it possible to interact with VsCoq?
Its not just coqtop (despite the name). There is an arg you can give it to set a different binary (for dune coq top). VsCoq uses coqidetop in the background and the path to that can be set from the settings. If you put dune coq top --toplevel=coqidetop
or something like that it should work.
I haven't actually tested this, but I have heard people managed to get it working.
I actually managed to make dune work with VsCoq well. In fact I only need to let _CoqProject maps to the binary generated by dune, then I can use Dune's output as testing, suggested here
But now I bump to "external library invisible for Coq Plugin Loader". According to that I should try use Coq 8.16 instead.
Ali Caglayan said:
I haven't actually tested this, but I have heard people managed to get it working.
I've tried that once and it didn't work. I had to go back to the _CoqProject
hack.
There are some changes to plugin loading in 8.16 which Dune 3.5 (just released) should be more suited for. Notably, the plugin must be loaded in a .v file using the public name i.e. Declare ML Module "mypackage.my.plugin"
. (there is also a "compat" syntax `Declare ML Module "my_plugin:mypackage.my.plugin") using both the "private" and public name.
In your Dune file, you should use the public name in the (plugins )
field for coq.theory
.
If you are using Dune, the compat syntax is mandatory in Declare ML Module
Unfortunately Dune 3.5 improves nothing until coqdep bugs are fixed
Last updated: Dec 07 2023 at 09:01 UTC