Stream: Coq devs & plugin devs

Topic: Building with Dune


view this post on Zulip Talia Ringer (Sep 08 2021 at 00:01):

Hi all, if I want to try to port my plugin to Dune, what libraries do I need to depend on? I'm trying coq-plugin-lib first: https://github.com/uwplse/coq-plugin-lib . I get a whole bunch of errors "unbound module Constr" "unbound module Environ" and so on

view this post on Zulip Talia Ringer (Sep 08 2021 at 00:02):

Paging @Emilio Jesús Gallego Arias who loves Dune

view this post on Zulip Pierre Roux (Sep 08 2021 at 05:48):

I guess those are in the kernel, probably coq-core.kernel?

view this post on Zulip Karl Palmskog (Sep 08 2021 at 06:52):

I think Emilio's Plugin template works well for understanding Dune (see my PR for how to make it work with 8.14 and beyond): https://github.com/ejgallego/coq-plugin-template

view this post on Zulip Karl Palmskog (Sep 08 2021 at 06:55):

Stalmarck has branches going back to v8.13 which combine extraction with Dune plugin building (tactic directory): https://github.com/coq-community/stalmarck


Last updated: Oct 21 2021 at 21:03 UTC