"Trigger must be tuples" error with single trigger expression

[Armael]

I tried using the trigger feature after reading the description in the CHANGELOG and examples from the testsuite. I'm getting a Trigger must be tuples error, and I can't figure out if there's a bug or if I'm doing something wrong and the error is just unclear.

Dummy example which triggers the error:

#[ensures(forall<x: Int> #![trigger(x + 1 - 1)] x + 1 - 1 == x)]
pub fn foo() {}

The error can be fixed by adding a stray comma at the end, but that seems wrong...:

#[ensures(forall<x: Int> #![trigger(x + 1 - 1),] x + 1 - 1 == x)]
pub fn foo() {}

[xldenis]

They don't have parentheses internally, look at this example:

#![trigger iter.produces(s.push(e1).push(e2), i), f.postcondition_mut((e1,), b)]

[Armael]

I still don't understand. According to the changelog the syntax should be of the form #![trigger e1,..,en], which means, I assume, #![trigger e] if there is only one trigger expression. This seems compatible with your example where there are two trigger expressions. On my example, (x + 1 - 1) is intended to be the trigger expression, hence my guess of #![trigger (x + 1 - 1)].

[xldenis]

Try removing the parentheses?

[Armael]

#![trigger x + 1 - 1] produces the same error (and seems difficult to parse unambiguously in more complex cases).

[xldenis]

I guess the parser needs to be improved, I suspect it is parsing parsing e, being repeated rather than e with , interspersed

[jhjourdan]

To be honest, I don't quite like the current syntax for triggers.

Sure, it follows Verrus, but it does not conform to the general syntax of Rust attributes, which is confusing. I tend to think that conforming to this syntax makes remembering the syntax easier, even if it is slightly heavier (two parentheses).

Cc @dewert99

[xldenis]

Sure, it follows Verrus, but it does not conform to the general syntax of Rust attributes, which is confusing

Actually in verus, they allow you to simply place #[trigger] next to an expression and that expression is used as the trigger. What we have currently is a hybrid of verus and viper.