Stream: Coq devs & plugin devs

Topic: Plugins with conflicting syntax


view this post on Zulip Li-yao (Nov 24 2020 at 13:56):

Say two plugins have VERNAC COMMAND EXTEND for the same command name, is there a reliable way to choose one over the other? Maybe loading one first/last?

In particular there's this issue that Equations and QuickChick both define Derive. I can add a QCDerive command, but should I also retire the existing Derive command, or is there a way for users of both packages to keep using Equation's version regardless?

view this post on Zulip Jakob Botsch Nielsen (Nov 24 2020 at 13:58):

I also asked here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Disambiguating.20between.20vernaculars.20from.20plugins

view this post on Zulip Li-yao (Nov 24 2020 at 14:04):

So if you load Equations last, you get its Derive?

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

Yep indeed. I think it would make sense to leave everything as it is in QC/Equations but just provide an additional unambiguous vernacular as an alias

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 16:42):

Hm, is that better or worse than "loading both plugins is forbidden" like for notations

view this post on Zulip Li-yao (Nov 24 2020 at 16:44):

It depends whether you are looking for an excuse to not work.


Last updated: Oct 16 2021 at 01:03 UTC