leanprover-community.github.io
leanprover-community.github.io copied to clipboard
leanprover-community
Add more exceptions to the naming rules to adhere with the current conventions
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
Could you split off the forking instructions to another PR and rename this one to something more evocative?
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)?
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. https://github.com/leanprover/lean4/pull/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 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.IsOpenfor 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?
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!
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).
Yes, I'm happy if you state the existence of exceptions. My preference is that we remove the
class LTexample, 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
CamelCasebecomescamelCasewhen 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!
@fpvandoorn OK, I was trying to set up to add some more instructions, and I got stuck in the ramifications of the site. For instance, there is https://leanprover-community.github.io/install/project.html and also https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency They do not contain the same information, they are accessible from different paths and the link https://leanprover-community.github.io/ci.html in the first one is broken.
Any suggestion on how to understand the whole structure?
Yes, it's a mess, and we should unify the instructions. I believe that https://leanprover-community.github.io/install/project.html is the easiest to find, so we need to make sure we keep that updated. We should add the way to create/modify projects within VSCode to that page.
I agree, and I am willing to contribute a bit. Do you know if the link https://leanprover-community.github.io/ci.html that appears in the middle of the page has been moved, deleted, other? And what about the whole "wiki" folder, that I cannot find on https://leanprover-community.github.io/ ?
I agree, and I am willing to contribute a bit. Do you know if the link https://leanprover-community.github.io/ci.html that appears in the middle of the page has been moved, deleted, other?
It looks like that page was deleted in https://github.com/leanprover-community/leanprover-community.github.io/commit/892d9086699a5676dbc4d24d7909c0ac9b1be212.
And what about the whole "wiki" folder, that I cannot find on https://leanprover-community.github.io/ ?
Hmm, I'm probably lacking context from not reading the entire discussion, but I don't know what wiki you're referring to here.
I agree, and I am willing to contribute a bit. Do you know if the link https://leanprover-community.github.io/ci.html that appears in the middle of the page has been moved, deleted, other?
It looks like that page was deleted in 892d908.
And what about the whole "wiki" folder, that I cannot find on https://leanprover-community.github.io/ ?
Hmm, I'm probably lacking context from not reading the entire discussion, but I don't know what wiki you're referring to here.
The one containing https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
Ah, I see. Yes, it would be good to at least link to the wiki or maybe copy / move the most useful instructions there.