Stream: Ltac2

Topic: Precedence of ";" with "by"

Michael Soegtrop (Mar 10 2021 at 13:59):

me again ...

I found that the precedence of ; in assert x by y; z seems to be different from Ltac1. As far as I can tell Ltac2 interprets assert x by y; z as assert x by (y; z) while Ltac interprets it as (assert x by y); z. Is this intentional?

Pierre-Marie Pédrot (Mar 10 2021 at 14:00):

Not that I know of.

Pierre-Marie Pédrot (Mar 10 2021 at 14:01):

Some precedences related to application were voluntarily changed, e.g. try and friends

Pierre-Marie Pédrot (Mar 10 2021 at 14:01):

But this one looks like a bug (?)

Pierre-Marie Pédrot (Mar 10 2021 at 14:03):

It's quite easy to fix, there is a clear difference between the Ltac1 and Ltac2 entry in this case.

Pierre-Marie Pédrot (Mar 10 2021 at 14:03):

(a missing level, as expected)

Michael Soegtrop (Mar 10 2021 at 14:22):

OK, thanks! Should I create an issue?

Pierre-Marie Pédrot (Mar 12 2021 at 08:12):

Please do.

Enrico Tassi (Mar 12 2021 at 08:41):

FTR, SSR's by would also read by (foo ; bar ; baz)

Enrico Tassi (Mar 12 2021 at 08:43):

According to my experience, this is what you want most of the times. (at least in interactive scripts)

Enrico Tassi (Mar 12 2021 at 08:45):

And it's precedence is always the same, it does not depend on what it follows

Michael Soegtrop (Mar 12 2021 at 18:04):

I just double checked Ltac1 again. It is indeed different as this snippet shows:

Goal 1=1.
Fail assert (1=1) by idtac; reflexivity.
assert (1=1) by (idtac; reflexivity).

So what shall we do? Make Ltac2 ssreflect compatible or Ltac compatible? I have no strong opinion on this. When it comes to non trivial tactics, they are all anyway quite different.

There are btw. a few other precedence differences, e.g. around repeat. Is the expectation that Ltac2 mimics Ltac as much as possible and deviations shall be reported?

Pierre-Marie Pédrot (Mar 12 2021 at 18:10):

The change of parsing for repeat is voluntary.

Pierre-Marie Pédrot (Mar 12 2021 at 18:10):

It's an issue many people have complained about for a long time.

Pierre-Marie Pédrot (Mar 12 2021 at 18:10):

(I mean, for Ltac1.)

Pierre-Marie Pédrot (Mar 12 2021 at 18:11):

So I decided for it to be a salient breakage introduced by Ltac2.

Pierre-Marie Pédrot (Mar 12 2021 at 18:11):

Same for try and similarly one-identifier tacticals.

Pierre-Marie Pédrot (Mar 12 2021 at 18:12):

They now all behave as if they were function applications (modulo the implicit thunk introduced by the syntactic notation)

Last updated: Apr 19 2024 at 05:01 UTC