tactic naming convention

Stream: lean4

[Leonardo de Moura]

We are moving forward to make the first Lean 4 official release. One issue is the naming convention for user-facing tactics.
We currently have tactics in snake_case (e.g., simp_all) and tactics in camelCase (e.g., rotateLeft).
Sebastian and I decided to use snake_case because simp_all and rotateLeft are keywords of the tactic language, and we have used snake_case for keywords in the rest of the language. Sorry for the inconvenience this change will create.

[Mario Carneiro]

@Leonardo de Moura By the way, there was a previous discussion about this at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20casing.20convention

[Leonardo de Moura]

@Mario Carneiro Thanks for posting it. The discussion seems to be inconclusive there. Any takeaways from your point of view?

[Mario Carneiro]

I think mac summarized the keyword convention perspective well in this post: If we think of tactics as keywords (which they technically are) then they should be snake cased, and if we think of them as functions then they should be camel cased. If we go snake case then I will have to update mathport since I had provisionally gone for camel case tactics, but I am mostly neutral on the question. (Snake case also helps avoid some uncomfortable questions about how to capitalize casesM or eRw or other tactics like that from lean 3.)

[Mario Carneiro]

Gabriel's point about set_option being consistently cased even if it exists as a tactic also seems persuasive

[Sebastian Ullrich]

Yes, tactics should be regarded as keywords. They're even already highlighted as such :) .

[Mario Carneiro]

ah, if they are highlighted then I guess that settles it

[Sebastian Ullrich]

The semantic highlighting simply highlights every identifier-like Syntax.atom as a keyword

[Mac]

Sebastian Ullrich said:

Yes, tactics should be regarded as keywords. They're even already highlighted as such :) .

Honestly, I think there is a little to much blue (i.e., keyword color) in Lean. Unlike most languages where there is a very small set of keywords, Lean's nonReservedSymbol parser and symbol leading behavior create a large set of pseudo-keywords. It would be nice if such pseudo-keywords (e.g., tactics) could have different syntax highlighting in some cases. For instance, if it was possible to highlight the leading token of a symbol leading behavior category differently. I think the discrimination would be quite pleasant to the eyes. In the short term, it might be worthwhile just to special case tactic for optionally different syntax highlighting.

Also, the distinction between true Lean keywords, user-defined keywords and pseudo-keywords is important for code in places like GitHub (or other such code presentation tools) which don't have semantic highlighting.

However, I don't have a particular string opinion on tactics names, and while I do think of tactics more like functions than keywords, I admit that using snake case for tactics does prevent naming clashes where actual keywords may be interweaved in proofs (like, potentially set_option).

[Mario Carneiro]

I don't think lean should try to make a distinction between keywords and pseudo-keywords. User defined commands and tactics should be just as legitimate as the builtins

[Mario Carneiro]

But having a different highlighting class for tactics is reasonable. In LSP you could even do it with a class name that is dynamically generated and depends on the category name, like keyword.control.lean.tactic

[Mario Carneiro]

that way custom themes can pick up on particular categories and highlight them differently

[Mac]

Mario Carneiro said:

I don't think lean should try to make a distinction between keywords and pseudo-keywords. User defined commands and tactics should be just as legitimate as the builtins

I actually agree with this! I think the fact that user-defined syntax is at the same level as builtin syntax is one of the great features of Lean. However, the fact still remains that they are different at some level and one should sometimes keep that in mind (depending on the application).

However, yeah, I think your suggestions are great and would love to see them in Lean at some point!