Stream: Coq devs & plugin devs

Topic: Plugins and grammars


view this post on Zulip Guillaume Melquiond (Feb 28 2023 at 15:03):

I have not quite followed what the various recent pull requests about plugins and parsers entail, but are they supposed to fix the following issue? (Script is currently accepted, should be rejected.)

Require ssreflect.
Goal True -> True.
idtac => H.

view this post on Zulip Pierre Roux (Feb 28 2023 at 15:09):

Why should it be rejected?

view this post on Zulip Guillaume Melquiond (Feb 28 2023 at 15:11):

Because just requiring ssreflect (possibly indirectly) should not modify the vanilla parser.

view this post on Zulip Pierre Roux (Feb 28 2023 at 15:16):

How should it be modified then?

view this post on Zulip Guillaume Melquiond (Feb 28 2023 at 15:19):

When doing Import ssreflect.

view this post on Zulip Enrico Tassi (Feb 28 2023 at 15:28):

I think that what you say is more true wrt tactic names than notations (whatever that means).
But I agree it is a bug, dunno how easy it is to fix.

view this post on Zulip Enrico Tassi (Feb 28 2023 at 15:28):

I mean, there are some chances that have is not in scope ;-)

view this post on Zulip Enrico Tassi (Feb 28 2023 at 15:29):

IIRC => is injected directly in the grammar, while have goes trough the tactic extension mechanism, which should honor Import

view this post on Zulip Guillaume Melquiond (Feb 28 2023 at 15:31):

Yes, there is a strange mix of both grammars. For example, it does not recognize the intro pattern //, but with a twist:

Syntax error: [ast_closure_term] expected after '/' (in [ssrfwdview]).

view this post on Zulip Gaëtan Gilbert (Feb 28 2023 at 15:34):

Guillaume Melquiond said:

I have not quite followed what the various recent pull requests about plugins and parsers entail, but are they supposed to fix the following issue? (Script is currently accepted, should be rejected.)

Require ssreflect.
Goal True -> True.
idtac => H.

no, they don't change that plugins act at Require time not Import time

Guillaume Melquiond said:

Yes, there is a strange mix of both grammars. For example, it does not recognize the intro pattern //, but with a twist:

Syntax error: [ast_closure_term] expected after '/' (in [ssrfwdview]).

probably because ssr has a hack to avoid changing the keywords at Require time

view this post on Zulip Guillaume Melquiond (Feb 28 2023 at 15:45):

I see. As long as Reserved Notation "//" has not been evaluated, the tokenizer does not recognize it as a token, and thus neither does SSReflect.


Last updated: May 18 2024 at 08:40 UTC