Guillaume Melquiond (Feb 28 2023 at 15:03): 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.
Why should it be rejected?
Guillaume Melquiond (Feb 28 2023 at 15:11):Because just requiring ssreflect (possibly indirectly) should not modify the vanilla parser.
Pierre Roux (Feb 28 2023 at 15:16):How should it be modified then?
Guillaume Melquiond (Feb 28 2023 at 15:19):When doing Import ssreflect.
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.
Enrico Tassi (Feb 28 2023 at 15:28):I mean, there are some chances that have is not in scope ;-)
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
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]).
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
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: Apr 20 2024 at 01:41 UTC