Stream: Coq devs & plugin devs

Topic: Introduce Base.Hash as extra OCaml dependencies for Plugin

view this post on Zulip Ende Jin (Feb 24 2023 at 05:11):

I am following for the plugin implementation. Now I have to use a Base.Hash (from Janestreet's Core) and thus introduce an external library.

I bump into the expected "Dynlink" error

Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/e5jin/project/FamilyPoly-Plugin/_build/default/src/fampoly_plugin.cmxs: undefined symbol: camlBase__Hash\")")

I am currently implementing my Coq plugin w.r.t. the Coq 8.15.0. I of course can try to update to 8.16.1 but I see someone failed to load appropriate library even with findlib

On the other hand, I currently only need Base.Hash. I kind of wonder how manually add library/dep works in Coq?

Last updated: Nov 29 2023 at 04:01 UTC