Stream: Coq users

Topic: Disambiguating between vernaculars from plugins


view this post on Zulip Jakob Botsch Nielsen (Nov 23 2020 at 09:24):

I have a project that uses both QuickChick and Equations. Both of these projects define the vernacular Derive X for Y. in plugins. Is there any way to disambiguate which vernacular I am referring to when I am in a file that has both plugins required?

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 09:25):

Depending on how those commands are defined, you can try your luck with Imports.

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 09:25):

Or redeclaring the ML modules that define them...

view this post on Zulip Jakob Botsch Nielsen (Nov 23 2020 at 09:34):

Loading the plugins in the opposite order indeed helps, so this helps, thanks!
One thing I noticed is that this has to be done from the beginning, it seems Declare ML Module is a no-op for plugins that are already loaded and does not "reoverride" the grammar

view this post on Zulip Jakob Botsch Nielsen (Nov 23 2020 at 09:38):

I guess that means there is no easy way to resolve the situation where you need both vernaculars in the same file, but that's probably acceptable. Maybe Equations and QuickChick should have some aliases prefixed with Equations and QuickChick to resolve this.

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 09:38):

Agreed. Maybe it would be worth to open issues in these projects.

view this post on Zulip Jakob Botsch Nielsen (Nov 23 2020 at 09:39):

Yep, I'll do that.


Last updated: Jan 28 2023 at 05:02 UTC