Using SerAPI as an external module in a Coq plugin

[efirst]

Hi! I'm trying to use SerAPI as an external module in a Coq plugin. On Zulip, Emilio gave me some pointers about using Declare ML Module in my plugin .v file and loading serapi+serapi dependencies manually before loading my plugin, but I'm still having issues.

I'm using Coq 8.9.1, ocaml 4.07.1, and coq_makefile to build my plugin with the command coq_makefile -f _CoqProject -o Makefile

I have a theories/Plib.v file for my plugin, which I've filled with:
Declare ML Module "plib". Add ML Path "/local/path/to/.opam/4.07.1+flambda/lib/coq-serapi/serlib". Declare ML Module "serlib".

And I added a Makefile.local, which I've filled with:
CAMLPKGS+= -package sexplib0 -package parsexp -package sexplib -package ppx_deriving -package coq-serapi

When I go to build this, I get the following warning:
COQDEP VFILES *** Warning: in file theories/Plib.v, declared ML module serlib has not been found!

So then, if I try to put open Serlib in my plibrary.ml4 file (which at the top has DECLARE PLUGIN "plib") I get the following error when I try to build:
CAMLOPT -pp -c -for-pack Plib src/plibrary.ml4 File "_none_", line 1: Error: Unbound module Serlib Hint: Did you mean Stdlib? make[1]: *** [src/plibrary.cmx] Error 2 make: *** [all] Error 2

I didn't include any path to serlib in my _CoqProject file, nor did I include Serlib in my plib.mlpack file.

How do I get it to recognize Serlib? Is including the serapi+dependencies in Makefile.local not adequate for loading them? Should I edit my _CoqProject and plib.mlpack files?

Any help is greatly appreciated. Thank you!

[ejgallego]

You can solve this now using the new findlib loader implement in Coq 8.16