best way to help?

Stream: mathlib4

[Arien Malec]

What would be the best way for an enthusiastic amateur to help the port? Happy to do grunt work, clean up documentation, do simple ports with supervision, etc.

Very conscious that enthusiastic but unskilled "help" can make things go more slowly, but if there's porting work tagged easy, etc, happy to pitch in...

[Moritz Doll]

if you want a miserable job, then finding theorems that have wrong names and correcting them is a great option. For instance docs4#Add.to_covariant_class_left should be called Add.to_covariantClass_left (you also should add an #align statement below the theorem).

[Moritz Doll]

example of such a PR is mathlib4#571

[Moritz Doll]

but this is really not fun/interesting

[Arien Malec]

Cool, so I'd fork Mathlib, grep for is_empty, and submit PRs for the corrections?

[Arien Malec]

I think "not fun grunt work" is probably my speed at first - the moral equivalent of giving a simple bugfix to a new developer.

[Arien Malec]

Or that work is already done, so take on your example above?

Is there docu for #align statements?

[Moritz Doll]

I think I changed all is_empty theorems, but I am completely sure

[Arien Malec]

Got it -- and is there a documented git workflow? work off branch to master, fork & PR, etc?

[Moritz Doll]

there is no documentation, it is just "#align $old_name $new_name" and you have to fully qualify the name

[Arien Malec]

I see the examples in your PR...

[Moritz Doll]

https://github.com/leanprover-community/mathlib4/wiki#aligning-names

[Moritz Doll]

as for github: do you have access to push to non-master branches? if not tell us your github username and someone will give you access and then the workflow is "create non-master branch and PR that"

[Arien Malec]

Github username: arienmalec

[Scott Morrison]

@Arien Malec, I've sent the invite.

[Arien Malec]

does an issue need to be open to accept the PR?

[Scott Morrison]

No

[Arien Malec]

apparently I committed to master rather than the branch?

[Arien Malec]

nevermind, figured it out...

[Arien Malec]

PR issued :fingers_crossed: that I did everything OK.

[Moritz Doll]

actually you did commit to master: https://github.com/leanprover-community/mathlib4/commit/2b62592b814921403d220112be7850059d211ed3

[Scott Morrison]

I guess it is time to protect master. :-)

[Scott Morrison]

@Arien Malec, can you use git revert, and push that, and then I'll protect it?

[Arien Malec]

yesh. Did that work?

[Arien Malec]

So I did git checkout -b arienmalec/covarientclass then git push -u origin arienmalec/covarientclass

[Arien Malec]

Looks like the revert took.

[Arien Malec]

apparently my git-fu was incorrect