Stream: Ltac2

Topic: Exposing Ltac2 variadic notations in Ltac1


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 17 2022 at 10:50):

you can have any arguments

view this post on Zulip Janno (Jul 22 2022 at 13:17):

This feature would be really, really nice to have. Is there a Coq issue tracking this?

view this post on Zulip Pierre-Marie Pédrot (Jul 22 2022 at 13:21):

No, but it would be very easy to implement.

view this post on Zulip Janno (Jul 22 2022 at 13:24):

How easy? :)

view this post on Zulip Pierre-Marie Pédrot (Jul 22 2022 at 13:24):

maybe 2h of work

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Janno (Jul 22 2022 at 13:30):

Oh, right, it needs a new toplevel command.

view this post on Zulip Janno (Jul 22 2022 at 13:32):

The most obvious choice might be Ltac2 in Ltac1 Notation .. := ...

view this post on Zulip Janno (Jul 22 2022 at 13:32):

Although that's already ambiguous, now that I read it again.

view this post on Zulip Gregory Malecha (Jul 22 2022 at 13:59):

can you use an attribute like #[ltac1_export] or something like that?

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 19:27):

See https://github.com/coq/coq/pull/16394 for a POC PR.

view this post on Zulip Janno (Aug 19 2022 at 07:46):

Cool! I'll take it for a spin right away.


Last updated: Dec 01 2023 at 06:01 UTC