wrong type of dot

Stream: mathlib4

[Rémy Degenne]

I wrote some code on a mathlib branch and after I pushed I got many linter errors of this type:
Error: Mathlib/Probability/Independence/Conditional.lean#L184: ERR_DOT: Line is an isolated focusing dot or uses . instead of ·
The dots are not isolated, so the error is the type of dot used. Before that, I never even saw that the dots at the beginning of tactic blocs were not the standard one. That raised several questions:

• how do I type the strange middle dot? It's not \cdot . The linter message could include that information.
• that's not an error in local, when typing #lint. Perhaps it could be? (or not, because it's perhaps a mathlib thing and we don't want to impose it to other projects?)
• and the obvious question: why don't we want to use the usual dot? It looks like TPIL uses the normal dot, for example.

I am not at all against using a middle dot for that purpose. It's just that I never realized that we were using a special character and I am curious about why that character was chosen.

[Rémy Degenne]

I guess I never realized the difference because it was not a linter error until #5708, which was merged two days ago

[Damiano Testa]

On my keyboard, the "middle dot" is AltGr + . where the . is the regular dot.

[Yury G. Kudryashov]

It should be \.

[Rémy Degenne]

Thanks! In the meantime, I opened a file in VSCode and hovered above a dot: it tells me it's \.

[Sebastian Ullrich]

I am curious about why that character was chosen

Because it looked nice, as a sort of bullet point list (which existed before in Coq, just with ASCII). This was introduced after the implicit lambdas already making use of \.

[Alex J. Best]

The style linters can also be run locally, but they are separate to the #lint framework, mostly just because they are normally simpler and written in python (so more of a lightweight check that runs even on code that doesn't actually build). There should be scripts to run these linters in the scripts folder and you could even set up your editor or git to run them at appropriate times for you as they should be very fast