naming convention: Cstar or CStar?

Stream: mathlib4

[Yury G. Kudryashov]

Should docs#CstarRing be named CStarRing, similarly to EReal?

[Ruben Van de Velde]

I always thought so

[Jireh Loreaux]

Probably

[Frédéric Dupuis]

It certainly looks better.

[Yury G. Kudryashov]

Current draft: #15495
Should I add some deprecated aliases?

[Eric Wieser]

One thing this raises: deprecations are of no use to users who have import Mathlib.Analysis.CstarAlgebra.Unitization at the top of their file

[Yury G. Kudryashov]

I don't know how can I help these users... Should we have "deprecated imports"? E.g., they can be implemented as files that import the new file and print a warning if they're imported. We'll have to update CI to allow them to be imported from Mathlib.lean (or have a list of exceptions to mk_all).

[Eric Wieser]

One big downside to deprecated imports is that I think git/github would then not track the renamed files, instead treating the file as brand new

[Eric Wieser]

Yury G. Kudryashov said:

Should I add some deprecated aliases?

I think deprecated aliases for the typeclasses alone should be enough

[Edward van de Meent]

Eric Wieser said:

One big downside to deprecated imports is that I think git/github would then not track the renamed files, instead treating the file as brand new

i don't think git history is something we care a lot about, since we already squash all commits...

[Edward van de Meent]

but if you want there to be a commit which notes the change, you can split the modification into two commits.

[Edward van de Meent]

it'll get squashed, but it'll exist somewhere

[Ruben Van de Velde]

Having files or folders side by side that only differ in case is probably going to wreak havoc on Windows

[Eric Wieser]

Edward van de Meent said:

i don't think git history is something we care a lot about

Git history is what is used for git blame, and git blame is really helpful for asking "why is this lemma the way it is".

Edward van de Meent said:

since we already squash all commits...

we tend to encourage moves and refactors to be done in separate PRs for this reason, but that doesn't apply here since the refactor is a trivial rename

[Yury G. Kudryashov]

#15495 is ready for review

[Damiano Testa]

Ruben Van de Velde said:

Having files or folders side by side that only differ in case is probably going to wreak havoc on Windows

In fact, I wrote a script to prevent paths that differ only by capitalization. I'm not sure that it still exists, but it was one of the CI steps for some time.

[Michael Rothgang]

The case-checker action still prevents that. (The check, just for Lean files, was part of lint-style.sh; I removed that check as it was duplicate.)