Naming of PreservesFiniteLimits.PreservesFiniteLimits

Stream: mathlib4

[Markus Himmel]

Is it correct that the sole member of the struct docs4#CategoryTheory.Limits.PreservesFiniteLimits should be called preservesFiniteLimits instead of PreservesFiniteLimits? Currently, it's inconsistent with docs4#CategoryTheory.Limits.PreservesLimitsOfShape, where the member is called preservesLimits, and if I understand the style guide correctly, starting with a lowercase letter is correct.

[Eric Wieser]

Yes, I agree that it should be lowerCamelCase

[Jeremy Tan]

image.png so it should be like this?

[Jeremy Tan]

!4#2827

[Jeremy Tan]

this is ready to merge

[Eric Wieser]

Any reason you tagged it with meta?

[Jeremy Tan]

It doesn't look that nice with just one tag

[Jeremy Tan]

fine I removed the meta tag

[Adam Topaz]

The meta tag is for PRs that have meta (as in metaprogramming) code.

[Thomas Murrills]

On mobile, but shouldn’t it also be preservesFiniteColimits (instead of PreservesFiniteColimits) in that file (in the analogous place)?

[Jeremy Tan]

Thomas Murrills said:

On mobile, but shouldn’t it also be preservesFiniteColimits (instead of PreservesFiniteColimits) in that file (in the analogous place)?

done

[Thomas Murrills]

Do we have a casing linter that can be turned on? :eyes: I mean, that’s kind of built into mathport, but maybe there’s some info when everything’s ported that informs the casing in ways which js occasionally invisible to mathport. It just makes me wonder what other fields might have slipped by…

[Jeremy Tan]

On a side note, very few files are being accepted today despite a fairly large haul of ready PRs

[Thomas Murrills]

It is a weekend, which might be contributing

[Thomas Murrills]

(Also there are relatively few people with merge powers anyway, I believe—so I’d guess times when they happen to be busy will naturally see fewer reviews and merges…I’m not sure we have enough ppl to average out such fluctuations, so to speak. But maybe we do! I haven’t looked at the numbers.)

[Eric Wieser]

Jeremy Tan said:

On a side note, very few files are being accepted today despite a fairly large haul of ready PRs

Note that the merge process is more than just someone with merge powers merging everything with a green checkmark; for port PRs, a reviewer has to look at the diff of commits[3:], and check that the porting changes all look reasonable

[Adam Topaz]

I wonder if @Matthew Ballard 's neovim setup is the culprit for all the whitespace ;)

[Eric Wieser]

I think mathport is to blame too, and/or start_port.sh

[Ruben Van de Velde]

Btw, if you want to help getting open pull requests landed, you can do an informal review before the maintainers get to it