good first port -- good beginner files

Stream: mathlib4

[Kevin Buzzard]

People interested in learning how to port files by doing it might want to watch Scott's video, but then what?

At the time of writing, here are a bunch of files which are (a) ready to be ported and (b) hopefully won't be too hard to port, in the sense that they don't use anything wacky like meta code.

alegbra.homology.complex_shape
data.stream.defs
data.typevec
control.ulift
algebra.quotient
order.game_add
data.two_pointing
data.vector3
data.mlist

If anyone is interested in trying one of these, then they should first check that nobody has claimed it since I wrote this message! They should check the port status page here, and if it's still unclaimed they can claim it e.g. by adding a comment WIP A. Porter, SHA 23482462384762384762837462378 on the port status page (copy the commit sha from the mathlib3port README ), and then they can go right ahead and copy the mathlib3port version of the file into a new mathlib4 file on a new branch and go right ahead and fix up the errors.

Note: the list in this message will go stale very quickly! Please check the port status page!

[Yaël Dillies]

(just claimed two_pointing)

[Kevin Buzzard]

Told you.

[Riccardo Brasca]

Be also sure to read the wiki. The video is very useful, but it's already outdated on some details (for example the SHA).

[Arien Malec]

Is data.mlist a thing? There's data.mllist but it uses unsafe so not sure it's a beginner project (I took a look and backed slowly away when I saw unsafe).

[Scott Morrison]

Yes, let's not bother porting data.mllist. It was only used in tactics.

[Scott Morrison]

I changed its status to No: probably not needed

[Arien Malec]

data.vector3 is only used in number_theory.dioph

[Scott Morrison]

That fine, lets port that.

[Scott Morrison]

(Obviously it's not high priority, but fine to practice on!)

[Arien Malec]

I'm being extra cautious about checking references :wink: