What to port?

Stream: mathlib4

[Sky Wilshaw]

I'm looking to start porting some of mathlib3 into mathlib4, and I want to find out what's free. I was thinking of working on Data.Multiset.Dedup and then Data.Multiset.FinsetOps, is anyone else working on these at the moment?

[Jireh Loreaux]

in a mathlib3 repo, you should run the port status script with ./scripts/port_status.py

[Jireh Loreaux]

This will tell you what currently needs porting.

[Scott Morrison]

(You won't be able to port those Multiset files yet, as various prerequisites are missing. You can use leanproject import-graph --to data.multiset.dedup --reduce --port-status --exclude-tactics out.pdf to generate a graph showing the prerequisites of that file, if for some reason you really want to aim there!)

[Sky Wilshaw]

Ah thank you, I was looking at mathport's generated imports to see the dependency tree, but they seem incomplete.

[Scott Morrison]

The current list of unclaimed ready-to-port files is:

algebra.order.monoid.order_dual
data.sigma.order
data.psigma.order

[Sky Wilshaw]

Right - there are more seemingly unclaimed files in the

# The following files have all dependencies ported already, and should be ready to port:

section, what is the difference with these ones?

[Scott Morrison]

Those ones have an unported transitive dependency, but all the immediate parents have been successfully ported, so with a bit of luck we can proceed anyway.

[Sky Wilshaw]

Ah, I see. One more question - do I need write access to mathlib4's non-master branches, or should I work from a fork and send in a PR later?

[Sky Wilshaw]

I might be misreading but it looks like it's the other way round - my port status execution looks like

# The following files have their immediate dependencies ported already, and may be ready to port:
order.with_bot    -- mathlib4#776 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
order.rel_iso.basic    -- PRed mathlib4#772
algebra.order.monoid.canonical.defs    -- WIP 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
algebra.order.monoid.order_dual    -- WIP by zeramorphic 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
data.prod.lex    -- PRed mathlib4#783 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
data.sigma.order
data.psigma.order

which seems to imply that the algebra.order.monoid.order_dual that you mentioned is one of those with only immediate dependencies but unported transitive dependencies.

[Scott Morrison]

It's best if you push from a branch, as CI works better that way.

[Scott Morrison]

If you tell me your github username I'll send an invite.

[Sky Wilshaw]

My username is zeramorphic, thanks!

[Sky Wilshaw]

Thank you!

[Scott Morrison]

Thanks, @Sky Wilshaw, I've left a comment on your PR. Almost good to go.