Stream: Coq devs & plugin devs

Topic: Turning a coq plugin to a library

Arpan Agrawal (Aug 14 2023 at 15:44):

I have a plugin that defines some Coq functions for use in other plugins. I was wondering if there's a way to use this plugin as a library (there's no reason it has to be a plugin, it was just written that way for convenience earlier) and use it as a dependency in another plugin. Does Dune provide a way to point to a specific commit of a repository for dependencies (currently we use build and load it as a git submodule).

Thanks!

Karl Palmskog (Aug 14 2023 at 15:59):

if you want to have a general-purpose OCaml library that's useful in an OCaml plugin for Coq, you might want to submit this as an opam package in the OCaml opam repository

Paolo Giarrusso (Aug 14 2023 at 19:08):

On your other question, that might be changing (I've seen issues), but at least yesterday's dune isn't a package manager so it won't deal with versions or fetch dependencies.

Arpan Agrawal (Aug 15 2023 at 18:19):

Is there an example/template for how to load plugins within other plugins? Especially if the dependency plugin is not released on opam

Paolo Giarrusso (Aug 15 2023 at 20:09):

How to load a plugin and how it's released (opam or not) are orthogonal. However, you probably want to build your plugin with dune https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20/35, and the other library should be a well-behaved library exposing findlib metadata (META files) — dune supports this. There was some issue but I forget if it was fixed already

Paolo Giarrusso (Aug 15 2023 at 20:11):

Relevant: https://github.com/ocaml/dune/issues/5998#issuecomment-1273399569 . The linked PR was merged in 8.17.1

Paolo Giarrusso (Aug 15 2023 at 20:13):

Regarding opam, I think using a git submodule is reasonable; if both projects build with dune, then dune should build both together pretty transparently — AFAIK that's pretty mature for OCaml.

Arpan Agrawal (Aug 16 2023 at 20:24):

Thanks for the pointers!

Arpan Agrawal (Aug 22 2023 at 17:04):

I followed the instructions to dynamically link the other plugin as a dependency. and when running dune build, I get the following warnings:

*** Warning: in file Fixtoelim.v, declared ML module example_plugin has not been found!
*** Warning: in file Fixtoelim.v, declared ML module elim_plugin has not been found!
*** Warning: in file Fixtoelim.v, declared ML module example_plugin has not been found!
*** Warning: in file Fixtoelim.v, declared ML module elim_plugin has not been found!

Where elim_plugin is the plugin I'm building that uses example_plugin as a dependency.
Am I doing something wrong here?

Here's the repository, running ./build.sh should be enough to reproduce the issue,

Thanks!

Paolo Giarrusso (Aug 22 2023 at 18:03):

But where are those plugins supposed to be coming from?

Arpan Agrawal (Aug 22 2023 at 18:50):

Elim_plugin is the one that's declared in Fixtoelim.v and example_plugin is loaded as a git submodule

Last updated: Dec 05 2023 at 12:01 UTC