the word "to"

Stream: new members

[Kevin Lacker]

it is annoying that naming your variable "to" works fine, until one happens to import something that recursively depends on tactic.lift, in which the word "to" is declared to be reserved notation

[Mario Carneiro]

maybe don't name your variable to then

[Kevin Lacker]

yeah now i know, this has been an enlightening experience chasing down why adding one more import causes a parse failure in unrelated code

[Mario Carneiro]

declaring a word as a token is a pretty big step, because it means no one is allowed to ever use it as a variable. This is a user facing design choice

[Mario Carneiro]

probably we should coalesce all token declarations in mathlib in one file that gets imported universally, like tactic.core or something

[Kevin Lacker]

it's just weird that I could make file A import file B, and that breaks a totally unrelated file C, because C happens to have a long dependency chain on A, and it uses the word "to"

[Mario Carneiro]

it's not that it uses the word to, it is that the file declares that to is now a keyword

[Kevin Lacker]

I mean that file C uses the word "to" as a variable name, an allegedly permitted maneuver

[Mario Carneiro]

C has the same issue when they declare new keywords

[Mario Carneiro]

There is a reason all the new keywords are weird things like co_await and reflexpr

[Kevin Lacker]

that usually happens when you push a new version of the language, though, not when someone adds import data.list.basic to some random library

[Mario Carneiro]

That's due to the extensible syntax design of lean

[Kevin Lacker]

anyway i just wanted to vent. thank you for feeling my pain. i'll go rename this stupid variable now

[Mario Carneiro]

it means libraries can literally extend the language in the same way as a new C version. This is huge for mathlib, we make extensive use of this capability

[Johan Commelin]

@Kevin Lacker I understand your pain. Do you think Marios suggestion would help?

[Johan Commelin]

Mario Carneiro said:

probably we should coalesce all token declarations in mathlib in one file that gets imported universally, like tactic.core or something

I mean :this:

[Kevin Lacker]

I don't really understand why this breaks, honestly, so I hesitate to support any particular solution

[Kevin Lacker]

I did not know about the reserve notation command until I discovered it was lurking in the weeds biting my ankle

[Mario Carneiro]

That's because you probably never thought to name a variable generalizing

[Mario Carneiro]

or using

[Mario Carneiro]

or at

[Mario Carneiro]

really any keywordy word that gets used in tactics

[Mario Carneiro]

ring implements a trick to allow it to recognize ring raw / ring SOP / ring horner without making those keywords

[Mario Carneiro]

Alternatively, we could change the preposition that lift uses

[Mario Carneiro]

there is a reason we reuse the same 3-4 words all over the place in tactic parsers

[Mario Carneiro]

how about lift x as int?

[Bryan Gin-ge Chen]

Isn't as much more commonly used, e.g. in lists a :: as?

[Mario Carneiro]

Right now I guess it's not a keyword, but I believe it used to be and at least some syntax highlighters think it still is

[Rob Lewis]

Mario Carneiro said:

probably we should coalesce all token declarations in mathlib in one file that gets imported universally, like tactic.core or something

I think this is a good idea and we don't need to change lift. As long as the variable to gets rejected immediately and not by some transitive import, it's not a big problem.

[Mario Carneiro]

can we get a style linter for this?

[Mario Carneiro]

I think it is as simple as grepping for reserve or precedence at the start of a line

[Bryan Gin-ge Chen]

I can work on a style linter for this when I get a chance.

[Bryan Gin-ge Chen]

#5330