Addin @alexkassil on github for port

Stream: mathlib4

[Alex Kassil]

Hello! I want to take a stab at helping the porting project. Following the guide here https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki, can I request someone add @alexkassil https://github.com/alexkassil to the mathlib4 github so I can help? Thanks!

[Alex Kassil]

Also, any tips for an easy first file to port? Looking at this https://leanprover-community.github.io/mathlib-port-status/ I find it hard to tell which is a good first port for beginners. I am chosing https://leanprover-community.github.io/mathlib-port-status/file/category_theory/bicategory/functor randomly

[Moritz Doll]

Given that obviously has not been ported, this might be a bit of a challenge. Generally, smaller files that have more theorems than definitions are easier to port.

[Alex Kassil]

@Moritz Doll Gotcha! Thanks for saving me time on that, going to go for a different file. Are any of https://leanprover-community.github.io/mathlib-port-status/file/combinatorics/catalan , https://leanprover-community.github.io/mathlib-port-status/file/data/finset/default , or https://leanprover-community.github.io/mathlib-port-status/file/data/bitvec/basic a good choice then?

[Johan Commelin]

Maybe data.fintype.card_embedding? (Has only 3 theorems, so probably very easy)

[Ruben Van de Velde]

catalan sounds fine. "default" files don't need porting

[Eric Wieser]

catalan has an open PR on the mathlib3 maintainer merge queue

[Eric Wieser]

So we should merge that (#16583) before porting

[Reid Barton]

Though it will no longer be ready for porting, after that.

[Reid Barton]

What's going on with the ? at
https://leanprover-community.github.io/mathlib-port-status/?q=data.rbtree.init

[Reid Barton]

Is it because the file has no imports?

[Eric Wieser]

Looks like I was lazy and did if deps where I meant if deps is not None

[Eric Wieser]

(None means "this file seems not to exist" and produces the ?)

[Eric Wieser]

Fixed

[Matthew Ballard]

When !4#1287 gets merged, category_theory.category.preorder might be a good first target.