Paolo Giarrusso (Apr 16 2022 at 22:02): Paolo Giarrusso (Apr 16 2022 at 22:02):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?
Paolo Giarrusso (Apr 16 2022 at 22:06):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).
Pierre-Marie Pédrot (Apr 17 2022 at 10:02):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.
Paolo Giarrusso (Apr 17 2022 at 10:21):In this example I'd only need the notation arguments, and I was hoping they could be parsed into ltac2 objects directly.
Pierre-Marie Pédrot (Apr 17 2022 at 10:49):I mean, what I propose is just a shorthand for ltac2:(foo) where foo is your notation, and you can just write foo inside Ltac1 verbatim.
Pierre-Marie Pédrot (Apr 17 2022 at 10:50):you can have any arguments
Janno (Jul 22 2022 at 13:17):This feature would be really, really nice to have. Is there a Coq issue tracking this?
Pierre-Marie Pédrot (Jul 22 2022 at 13:21):No, but it would be very easy to implement.
Janno (Jul 22 2022 at 13:24):How easy? :)
Pierre-Marie Pédrot (Jul 22 2022 at 13:24):maybe 2h of work
Pierre-Marie Pédrot (Jul 22 2022 at 13:25):(the change in itself is probably shorter to write, but you have to take the overhead of tests and whatnot)
Janno (Jul 22 2022 at 13:25):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
Pierre-Marie Pédrot (Jul 22 2022 at 13:25):I have one and half hour in front of me, let's start writing this
Pierre-Marie Pédrot (Jul 22 2022 at 13:26):the notation stuff is already there, it's only about plugging it into the Ltac grammar
Pierre-Marie Pédrot (Jul 22 2022 at 13:28):the hardest thing to solve is to settle down for a precise syntax for the command (aka the urumheit of bikeshedding)
Janno (Jul 22 2022 at 13:30):Oh, right, it needs a new toplevel command.
Janno (Jul 22 2022 at 13:32):The most obvious choice might be Ltac2 in Ltac1 Notation .. := ...
Janno (Jul 22 2022 at 13:32):Although that's already ambiguous, now that I read it again.
Gregory Malecha (Jul 22 2022 at 13:59):can you use an attribute like #[ltac1_export] or something like that?
Pierre-Marie Pédrot (Jul 22 2022 at 14:22):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.
Pierre-Marie Pédrot (Aug 18 2022 at 19:27):See https://github.com/coq/coq/pull/16394 for a POC PR.
Janno (Aug 19 2022 at 07:46):Cool! I'll take it for a spin right away.
Last updated: Apr 20 2024 at 07:01 UTC