Talia Ringer (Sep 08 2021 at 00:01): 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
Talia Ringer (Sep 08 2021 at 00:02):Paging @Emilio Jesús Gallego Arias who loves Dune
Pierre Roux (Sep 08 2021 at 05:48):I guess those are in the kernel, probably coq-core.kernel?
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
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: Apr 19 2024 at 21:01 UTC