Global or scope syntax in mathlib4

Stream: mathlib4

[Nicolas Rouquette]

Mathlib4 defines lots of global syntaxes like this one:

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/StacksAttribute.lean#L134

namespace Mathlib.StacksTag

...

syntax "stacks" : stacksTagDB

With just import Mathlib.Tactic, the Lean parser effectively treats stacks as a reserved keyword.
In a file Foo.lean, I had something like this:

structure Foo where
   stacks : List String

Ok, no problem so far; elsewhere, I had:

import Foo
import Mathlib.Tactic

def kaboum : Foo where
   stacks := []

Now, I get confusing error messages:

• at "where": Fields missing: stacks
• at "stacks": unexpected token 'stacks'; expected command

There are at least two ways to work around this:

1) Escape the symbol when Mathlib.Tactic is imported

def kaboum : Foo where
   «stacks» := []

2) Globally scope the syntax definition

In Mathlib/Tactic/StacksAttribute.lean:

namespace Mathlib.StacksTag

...

global syntax "stacks" : stacksTagDB

However, this would require an explicit open Mathlib.StacksTag for the parser to recognize it.

With 183 definitions of "syntax ..." in Mathlib.Tactic, there's a high likelihood that someone else will trip on this name collision.

What should we do about this?

[Aaron Liu]

make it non-reserved

[Nicolas Rouquette]

@Aaron Liu Can you elaborate what this means?

[Robin Arnez]

Non-reserved means don't treat stacks as a keyword but instead make it parse from the identifier "stacks".

[Aaron Liu]

it means you can use it in the syntax without becoming a reserved token (so you can also use it as just a name), for example docs#Lean.Parser.Tactic.tacticRfl is a tactic but it's nonreserved so docs#rfl is a term and you can refer to it without having a conflict
see also docs#Lean.ParserDescr.nonReservedSymbol docs#Lean.Parser.nonReservedSymbol docs#Lean.Parser.Syntax.nonReserved docs#Lean.Parser.LeadingIdentBehavior

[Nicolas Rouquette]

@Aaron Liu Thanks for the pointers.

If I understand well, the suggestion would be to change the way Mathlib.Tactic syntactic symbols are defined.

Instead of:

syntax "stacks" : stacksTagDB

We'd have:

syntax (nonReservedSymbol "stacks") : stacksTagDB

or:

def stacksDB := Lean.Parser.nonReservedSymbol "stacks"
syntax stacksDB : stacksTagDB

There are pros/cons to scoped vs. nonReservedSymbol:

Approach	Pros	Cons
scoped syntax	Explicit opt-in	Requires open everywhere the attribute is used
nonReservedSymbol	Works globally, doesn't break identifiers	Slightly more complex syntax definition

Should we apply this change to all 183 Mathlib.Tactic syntax definitions?

(do grep -r '^syntax ' Mathlib/Tactic/**/*.lean in your copy of Mathlib4)

[Aaron Liu]

I'm thinking we should instead change the leading ident behavior of the syntax category stacksTagDB

[Ruben Van de Velde]

By the way, stacks is only used for attributes, right?

[Nicolas Rouquette]

Ruben Van de Velde said:

By the way, stacks is only used for attributes, right?

I'm not an expert on Mathlib Tatics; hopefully someone can answer that question.

Regarding the proposition to use a non-reserved symbol, the proper incantation w/ Lean 4.27.0-rc1 is:

-- makes "stack" a non-reserved symbol
syntax &"stacks" : stacksTagDB

[Kim Morrison]

Did this get fixed? A PR would be great.

[Aaron Liu]

I guess I'll put something toger

[Aaron Liu]

well I tried it and it doesn't work

[Aaron Liu]

doing &"stacks" instead of "stacks" fails because it parses it as a docs#Lean.Parser.Attr.simple

[Aaron Liu]

and doing (behavior := symbol) or (behavior := both) leads to ambiguous parsing when you have stuff like @[kerodon 0X12] in which there's no additional comment and the tag can be interpreted as either an identifier or a number literal (or more generally anything of syntax category docs#Lean.Parser.Category.prio) (this is also due to docs#Lean.Parser.Attr.simple)

[Aaron Liu]

and this gives you the wonderful error "Unknown attribute [choice]" because the parser wraps the two options in a choice node and for some reason it's interpreted as the name of the attribute