Camel case for test files

Stream: mathlib4

[Yaël Dillies]

Should test files in mathlib be camelCased or snake-cased? Right now, we have a bit of both.

[David Renshaw]

My impression is that the snake-cased ones are vestiges from Lean 3.

[Bryan Gin-ge Chen]

Do we have a linter for file names? If so, maybe we should make it run on MathlibTest.

[Ruben Van de Velde]

We talked about one for windows-invalid file names. I think that landed? Probably it could easily be extended

[Yaël Dillies]

In fact, the OS-invalid filenames linter is a derivative of the then already existing camel-case filename linter :laughing:

[Michael Rothgang]

I prefer UpperCamelCase (like mathlib modules, and be it for consistency).

[Michael Rothgang]

My understanding was that there's a weak consensus for this, but nobody cared enough to rename all the files.

[Eric Wieser]

What does lean core do for their tests?

[Eric Wieser]

https://github.com/leanprover/lean4/tree/master/tests/lean is mostly lowerCamelCase

[Mario Carneiro]

David Renshaw said:

My impression is that the snake-cased ones are vestiges from Lean 3.

Nope, at least for a while I was deliberately snake casing all test files, e.g. interval_cases tactic would have a test file called interval_cases.lean. Having a different naming convention also helps notice that it's not a regular file