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):

Hi
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?
Thanks!

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: https://github.com/coq/coq/pull/15220

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.


Last updated: Feb 05 2023 at 20:03 UTC