Mention that some fields are currently lowercase, not following the current conventions

[faenuccio]

Modify the instructions in the naming convention file about LT vs lt and add a new example.

Add a sentence requiring to fork before creating a PR in the readme.md file

[fpvandoorn]

Did you intend to remove this example?

[faenuccio]

Not really, as I have amended rule 6.

[faenuccio]

@fpvandoorn It seems to me this PR got somewhat stuck...

[YaelDillies]

Could you split off the forking instructions to another PR and rename this one to something more evocative?

[faenuccio]

Could you split off the forking instructions to another PR and rename this one to something more evocative?

Sure (although I am boarding a plane now and it won't be immediate). Can you just tell me if the forking instructions are OK or if they would at any rate be ignored "because they're so trivial" (something I often hear, but I would argue that a superfluous instruction makes no harm to those who know and can help those who don't)?

[faenuccio]

Done (and opened #471 )

[fpvandoorn]

I think the issue here is that you're documenting exceptions as the rule.
The goal is to have propositions UpperCamelCased, with very few exceptions.
E.g. leanprover/lean4#1897 shows that we want to get rid of some of the exceptions, but just haven't gotten around to it yet.
The naming file is prescriptive, not descriptive. So even though currently we might not capitalize all propositional fields, we want to do that more. So I don't think we want to make a rule in the naming conventions that we lowercase certain fields.
Moreover, many fields that are propositions are capitalized: TopologicalSpace.IsOpen for example.

[faenuccio]

I think the issue here is that you're documenting exceptions as the rule. The goal is to have propositions UpperCamelCased, with very few exceptions. E.g. leanprover/lean4#1897 shows that we want to get rid of some of the exceptions, but just haven't gotten around to it yet. The naming file is prescriptive, not descriptive. So even though currently we might not capitalize all propositional fields, we want to do that more. So I don't think we want to make a rule in the naming conventions that we lowercase certain fields. Moreover, many fields that are propositions are capitalized: TopologicalSpace.IsOpen for example.

I see your point, and agree. Yet I find it a bit frustrating (and I'm not alone, in view of recent LFTCM experience) that the library is full of exceptions. Would you agree if I modify my text explicitly mentioning that there are exception to the rule(s), but that these will hopefully eventually disappear and users should adhere to the rules rather than trying to mimic what they find in the library?

[fpvandoorn]

Yes, I'm happy if you state the existence of exceptions.
My preference is that we remove the class LT example, since that itself is an exception.
If we keep it, we should explicitly write that this is an exception to the rule.

Aside: I haven't noticed the "uncapitalize projection fields" as a big naming issue myself. All lemmas are still correctly named, since a declaration CamelCase becomes camelCase when it is part of a lemma name.

And btw, please add more "trivial" steps to our Git instructions on the website. They are very hard for mathematicians to follow! Please incorporate the instructions from the Git tutorial at LFTCM that I gave into the website!

[faenuccio]

I have added the LT exception and will add more GIT instructions as they come to mind. One thing that I would like to discuss (but completely outside this PR) is the confusion between the Lean and the Math community in the website: it is called "Lean Community" but basically only speaks about Mathlib. For instance, the GitHub link on the left points to mathlib (hence I would, a minima suggest that it becomes Mathlib repository or something).

[fpvandoorn]

2 wrongly spaced things (I'll fix them myself), otherwise, this looks good to me.