Iris uses variadic Ltac1 notations, implemented as usual. Ltac2 can do better, but the resulting notations are only available in Ltac2 mode (or via
Ltac2). How hard would it be plugging Ltac2 notations into the Ltac1 parser?
While the existing notations already work, the current approach complicates adding new ones (as in https://gitlab.mpi-sws.org/iris/iris/-/issues/452#note_80114).
It's not very hard to also import Ltac2 notations directly as Ltac1 entries, I've been thinking about that for a bit already. But it's going to be problematic if you want to refer to Ltac1 bound variables inside the Ltac2 tactic. The only sane way is to forbid this, i.e. you can't never refer to a Ltac1 variable from such notations.
In this example I'd only need the notation arguments, and I was hoping they could be parsed into ltac2 objects directly.
I mean, what I propose is just a shorthand for
foo is your notation, and you can just write
foo inside Ltac1 verbatim.
you can have any arguments
This feature would be really, really nice to have. Is there a Coq issue tracking this?
No, but it would be very easy to implement.
How easy? :)
maybe 2h of work
(the change in itself is probably shorter to write, but you have to take the overhead of tests and whatnot)
Wow, I am positively surprised by this. I can't remember the last time anything I wanted to do took only 2 hours and I am not working on Coq notation internals :D
I have one and half hour in front of me, let's start writing this
the notation stuff is already there, it's only about plugging it into the Ltac grammar
the hardest thing to solve is to settle down for a precise syntax for the command (aka the urumheit of bikeshedding)
Oh, right, it needs a new toplevel command.
The most obvious choice might be
Ltac2 in Ltac1 Notation .. := ...
Although that's already ambiguous, now that I read it again.
can you use an attribute like
#[ltac1_export] or something like that?
I have to go, but there are unexpected trouble related to the self and next entries of Ltac2, because we're not in a context where we're parsing Ltac2 expressions anymore. I will have to clean that up a bit first.
See https://github.com/coq/coq/pull/16394 for a POC PR.
Cool! I'll take it for a spin right away.
Last updated: Dec 01 2023 at 06:01 UTC