Stream: Dune devs & users

Topic: Detection of plugins used by a .v file


view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2023 at 19:07):

Hi folks,

I'm continuing the discussion on https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/Dune.203.2E8.20theories.20declarations about a request that I think is orthogonal of the original bug here.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2023 at 19:09):

@Ali Caglayan mentions the possibility to actually guess automatically what plugins are in use by a theory.

Before Coq 8.16, that was not easy to do, as the Declare ML Module syntax didn't include a proper name. However, for Coq 8.16, indeed, if a .v file is using the new syntax, indeed Dune could compute the (plugins ...) fields needed for the plugins automatically.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2023 at 19:09):

So maybe we should document the plan as a Dune issue, and implement this eventually.


Last updated: Oct 13 2024 at 01:02 UTC