Stream: Coq devs & plugin devs

Topic: Setup Development Environment for Coq Plugin

Ende Jin (Oct 19 2022 at 19:50):

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.

1. I am sure this is not the correct way to engineer. Is there an (officially/widely-recognised) best engineering practice to do this?
2. Currently I want to use a third-party library of OCaml but I have no idea how to configure coqproject/coqmakefile to add those dependencies. I tried to find documentation or any existent plugin example for illustration but I failed.

Ali Caglayan (Oct 19 2022 at 21:12):

There is a plugin example in the Dune docs too: https://dune.readthedocs.io/en/stable/coq.html#coq-plugin-project

Ali Caglayan (Oct 19 2022 at 21:13):

Using both coq_makefile and Dune will be tricky. You should be able to do everything with Dune.

Ende Jin (Oct 20 2022 at 00:35):

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?

Ali Caglayan (Oct 20 2022 at 01:07):

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.

Ali Caglayan (Oct 20 2022 at 01:07):

I haven't actually tested this, but I have heard people managed to get it working.

Ende Jin (Oct 20 2022 at 03:55):

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.

Théo Zimmermann (Oct 20 2022 at 07:21):

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.

Ali Caglayan (Oct 20 2022 at 11:37):

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.

Ali Caglayan (Oct 20 2022 at 11:38):

In your Dune file, you should use the public name in the (plugins ) field for coq.theory.

Emilio Jesús Gallego Arias (Oct 20 2022 at 12:41):

If you are using Dune, the compat syntax is mandatory in Declare ML Module

Emilio Jesús Gallego Arias (Oct 20 2022 at 12:42):

Unfortunately Dune 3.5 improves nothing until coqdep bugs are fixed

Last updated: Dec 07 2023 at 09:01 UTC