lean3port

Stream: mathlib4

[Kevin Buzzard]

lean_core.data.vector is on the most wanted list; this is data.vector from Lean 3 core. Did someone mention that there was a way to get an autoported version of this file somehow? I'm looking for a porting job.

[Scott Morrison]

Yes, there is the lean3port repository, just like the mathlib3port repository.

[Moritz Doll]

Kevin, if you are out of work: mathlib4#674 has some rather weird coercion errors and Arien has asked for help with that

[Kevin Buzzard]

OK I'll look at 674 for now :-) Thanks both!

[Siddhartha Gadgil]

Is the ported file supposed to be Mathlib/Lean/Data/Vector.lean (or just Mathlib/Data/Vector.lean )?

[Scott Morrison]

If you are porting a file from lean 3 core, it should go in Mathlib/Init/.

[Scott Morrison]

(The Mathlib/Lean/ folder is for add-ons to Lean 4 core that are for now residing in mathlib4.)

[Siddhartha Gadgil]

I was looking at the Vector.lean file and it seems that it uses List.map₂ and some other functions that are not ported. Was this missed in saying lean_core.data.vector is ready to port or am I missing something?

[Scott Morrison]

I would not trust the port_status.py script when it comes to analysing what is ready to port from lean 3 core. It is not attempting to analyse anything there at all, and the fact that lean_core.data.vector is shown on the list is more or less a bug to begin with.

[Siddhartha Gadgil]

Scott Morrison said:

I would not trust the port_status.py script when it comes to analysing what is ready to port from lean 3 core. It is not attempting to analyse anything there at all, and the fact that lean_core.data.vector is shown on the list is more or less a bug to begin with.

Thanks. Would the correct approach be to port this to Mathlib/Init/ and also create a file there /Mathlib/Init/List/BasicExtras.lean with functions that were in Lean 3's list/basic.lean but were dropped from Lean 4's List/Basic.lean?

[Scott Morrison]

Anything that is still unported from Lean 3 core's list/basic.lean belongs in Mathlib/Init/List/Basic.lean

[Scott Morrison]

no need for BasicExtras: the fact that it is in Mathlib/Init/ is enough.

[Eric Wieser]

Scott Morrison said:

Anything that is still unported from Lean 3 core's list/basic.lean belongs in Mathlib/Init/List/Basic.lean

Where do things in Lean3 core's init/data/list/basic.lean belong then?

[Eric Wieser]

Scott Morrison said:

If you are porting a file from lean 3 core, it should go in Mathlib/Init/.

I think this rule might be wrong; isn't it "if you are porting a file from the init folder in lean3 core, it belongs in Init, otherwise if not it belongs not in Init"?

[Mario Carneiro]

I agree with Eric: init.data.list.basic -> Mathlib.Init.Data.List.Basic and data.vector -> Mathlib.Data.Vector

[Siddhartha Gadgil]

Working on this. Will update the wiki.

[Siddhartha Gadgil]

Wasn't sure if one should alert about PRs here too. In any case https://github.com/leanprover-community/mathlib4/pull/834 does the following (I hope)

• port Mathlib.Data.Vector
• port a handful of definitions and lemmas needed for this that are not (yet?) in Std4.