Stream: Coq devs & plugin devs

Topic: ✔ Use Micromega_plugin in another plugin, in Coq-8.16

view this post on Zulip Chantal Keller (Oct 11 2022 at 15:03):

In SMTCoq, I use the Micromega plugin at the OCaml level. I used to refer to it by Micromega_plugin. ... but when porting to Coq-8.16 I get Error: Unbound module Micromega_plugin. How can I refer to it? Do I need to add something in some lookup path?

view this post on Zulip Pierre Roux (Oct 11 2022 at 15:09):

Sounds like the move to findlib for loading plugins, you can probably take inspiration on the overlay pull requests listed in the initial pull request:

view this post on Zulip Guillaume Melquiond (Oct 11 2022 at 15:10):

You need to instruct ocamlfind to find it, e.g., with -package coq-core.plugins.micromega.

view this post on Zulip Chantal Keller (Oct 11 2022 at 15:17):

Many thanks to both of you, that helped me solve my problem, and also understand better what to put in my own -generate-meta-for-package and Declare ML Module.
By the way, I do not find the documentation really clear about pkg and foo.

view this post on Zulip Notification Bot (Oct 12 2022 at 08:22):

Chantal Keller has marked this topic as resolved.

Last updated: Dec 07 2023 at 09:01 UTC