permission for mathlib4?

Stream: mathlib4

[Jake Levinson]

Hi, I'd like to help out with the porting effort. Can I get permission for mathlib4? Or do I already have it since I have it for mathlib3? I'm jakelev on github.

[Scott Morrison]

@Jake Levinson, invite sent!

[Jake Levinson]

Okay, I've tried a couple of different files (algebra.category.GroupWithZero and topology.algebra.equicontinuity) and in both cases ran into errors involving coercions and metavariables, where Lean 4 is failing to infer implicit arguments that Lean 3 did automatically.

I'm not sure how to fix these since it doesn't seem like a matter of just renaming things. Would anyone be up for pair-programming or otherwise helping me debug one of these?

Or, anyone have a suggestion for how to find an easier first file to port? (I just looked for short, greenlisted files on the porting status page.)

[Moritz Doll]

If you make a wip-PR, then I can take a look this evening (i.e. in ~4h). Generally what I am doing is (a) insert the arguments explicitly (b) use some of the workarounds for the instance-eta-problem (c) compare with mathlib3 to see how the goals and lemmas differ. Looking into the porting notes for files that your file directly depends on might help as well since the problems usually are closely related.

[Jake Levinson]

Hey thanks! Alright, I will do that. Those sound like good steps though I probably will need help executing them at first - still getting used to the differences between Lean 3 and 4.

[Jake Levinson]

@Moritz Doll see !4#3841