Ende Jin (Feb 24 2023 at 05:11): Ende Jin (Feb 24 2023 at 05:11):I am following https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20 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: Apr 20 2024 at 01:41 UTC