newer ports

Stream: PR reviews

[Jeremy Tan]

!4#3389 forward ports 4 mathlib3 commits

[Jeremy Tan]

Not sure though if it should be SimpleGraph.ConnectedComponent.inhabited or SimpleGraph.**c**onnectedComponent.inhabited, though I lean towards the former

[Jeremy Tan]

!4#3245 is fixed and ready to merge (again)

[Jeremy Tan]

Ready for review:
!4#3063
!4#3315
!4#3437
!4#3441
!4#3405

!4#3439
!4#3443

[Jeremy Tan]

!4#3444 is ready for review – in true Riou style it begins a long chain of PRs

[Jeremy Tan]

!4#3453 is ready

[Jeremy Tan]

!4#3386

[Jeremy Tan]

!4#3455

[Jeremy Tan]

!4#3401

[Jeremy Tan]

!4#3454
!4#3456

[Jeremy Tan]

!4#3338
!4#3343

[Jeremy Tan]

!4#3211
!4#3458

[Eric Wieser]

Note that it's not really necessary for you to post all of the ready PRs; we have #queue4 which automatically sorts by the right thing

[Jeremy Tan]

You should probably make #queue4 sort by "Recently updated" rather than "Least recently updated"?

[Eric Wieser]

The idea is to catch long-forgotten PRs.

[Eric Wieser]

In practice though the order at #port-dashboard is probably more useful during porting

[Jeremy Tan]

The homology hype train continues:
!4#3492
!4#3493
!4#3468
!4#3491
!4#3495

[Jeremy Tan]

Other stuff:
!4#3494
!4#3496 -> !4#3498
!4#3499

[Jeremy Tan]

!4#3471 – tactic port, needed for LinearAlgebra.FiniteDimensional

[Jeremy Tan]

!4#3468 is (again) ready to merge

[Jeremy Tan]

!4#3357 (Topology.MetricSpace.Polish)
!4#3501 (aesop bump)
!4#3500 (AlgebraicTopology.CechNerve)
!4#3463 (CategoryTheory.Sites.Limits)
!4#3508 (forward port)
!4#3405 (Data.Seq.WSeq)
!4#3506 (Data.Complex.Cardinality)
!4#3513 (Analysis.NormedSpace.BallAction)
!4#3515 (Algebra.Category.ModuleCat.Products)
!4#3206 (Logic.Equiv.TransferInstance) -> !4#3505 (CategoryTheory.Preadditive.Opposite)
!4#3514 (RingTheory.Localization.Submodule)

[Patrick Massot]

@Jeremy Tan please carefully reread https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/newer.20ports/near/350270643

[Jeremy Tan]

!4#3106 and !4#3480 were marked as ready to merge but bors has not actually merged them

[Jeremy Tan]

Other stuff ready for review:
!4#3662, !4#3657, !4#3510

[Jeremy Tan]

!4#3793 was prematurely sent to bors and the build failed. It has since been fixed and is ready again

[Eric Wieser]

Thanks for the reminder, I was waiting to confirm the build was happy.

[Eric Wieser]

Hmm, I unfortunately can't seem to leave any comments on github right now

[Jeremy Tan]

Another sledgehammer style PR is ready for review, this one involving by: !4#3825

[Eric Wieser]

It's tempting to leave this type of style cleanup to an auto-formatter

[Eric Wieser]

We don't really have one yet, but developing one would in the long term be a better use of time than doing stuff manually

[Jeremy Tan]

I actually have ready a small addition to the style linter that checks for such "isolated bys", but I'll wait for @Mario Carneiro to finish reviewing

[Mario Carneiro]

yes, I definitely came out of this wanting an auto-formatter

[Eric Wieser]

A linter change is certainly better than nothing

[Jeremy Tan]

CI is now green for !4#3825

[Jeremy Tan]

!4#3942 failed at merging because of a lint error, I've fixed it, it can be merged again now

[Jeremy Tan]

Same for !4#3945

[Jeremy Tan]

!4#3938, by its very nature of changing the naming convention around sups and infs, should probably be merged as soon as possible because new PRs are still coming in with the old names and they may cause either merge conflicts or new things that break

[Eric Wieser]

I don't know if we reached consensus on that rename yet

[Eric Wieser]

Ah, it's been merged anyway

[Jeremy Tan]

!4#4014 can be merged now

[Jeremy Tan]

Our out of sync queue is getting very long… a lot of the forward porting PRs are ready for review.

The following 31 files at 33c67ae6 have been modified in mathlib3 since the commit at which they were verified.

[Jeremy Tan]

Also !4#4018 (MeasureTheory.Constructions.BorelSpace.Basic) has just been sitting there ready to review for some days now

[Eric Wieser]

!4#4007 alone will get the queue down to 21

[Eric Wieser]

@Felix Weilacher, note that #18962 added three items to this list; it would be great if you could make a PR to forward-port them!

[Felix Weilacher]

Apologies, I have been traveling and may not be able to get to it for a day or two.

[Eric Wieser]

Don't worry, it's not urgent! But it should probably be higher up your list than any further contributions to mathlib3.

[Jeremy Tan]

!4#4156 and !4#4186 were marked ready to merge but have not actually been merged

[Patrick Massot]

There are merge conflicts

[Patrick Massot]

according to bors at least

[Jeremy Tan]

I'd like to get a review of !4#4420 (InnerProductSpace.PiL2), which is one of the target files in port progress.

Also !4#4441 (Analysis.Calculus.Deriv.Pow) has not been reviewed or delegated

[Eric Wieser]

I was going to look at that second one shortly

[Jeremy Tan]

Now I'd like !4#4422 to be reviewed and merged, so that !4#4431 can be merged

(for the same reason as here)

[Jeremy Tan]

!4#4447 (Analysis.Calculus.Deriv.ZPow) should be ready for review even though it doesn't have the tag

[Eric Wieser]

We should wait for @Yury G. Kudryashov to confirm that it is actually ready for review

[Eric Wieser]

It doesn't look ready to me, I imagine the plan is to rebase the commits first

[Jeremy Tan]

In the meantime, what about reviewing/merging !4#4508

[Jeremy Tan]

(which is a prereq for MeanValue)

[Yury G. Kudryashov]

@Jeremy Tan Thank you for pushing my PRs. I'll rebase Deriv.ZPow in ~30m.

[Yury G. Kudryashov]

I'm at a family vacation and may not be available as often as usual.

[Yury G. Kudryashov]

Rebased ZPow, marked as awaiting-review.

[Yury G. Kudryashov]

I'll fix MeanValue tonight. The next big roadblock in the *deriv branch of calculus is a timeout in !4#4256 (ContDiffDef). I tried to fix it several times and failed.