porting requests

Stream: mathlib4

[Mario Carneiro]

Since we have a wide open space of files to port at the moment, I thought I would make a thread for people to request specific files to get them bumped up in priority.

[Mario Carneiro]

• algebra.invertible: I'm going to need parts of this for norm_num, although I can work around it for now.

[Scott Morrison]

For which

leanproject import-graph --to algebra.invertible --exclude-tactics --port-status algebra.invertible.pdf

says algebra.invertible.pdf.

[Scott Morrison]

This may be a case where refactoring the file in mathlib3 to isolate the parts you need might be warranted first.

[Mario Carneiro]

yikes

[Scott Morrison]

Yeah, import creep is vicious. :-)

[Mario Carneiro]

I remember the days when stuff in "algebra" was supposed to have low dependencies

[Mario Carneiro]

I think it was a poor choice of name

[Scott Morrison]

Most of this tree is transitive imports via algebra.order.ring and data.set.lattice. I suspect very large portions of algebra.invertible don't need anything from either of those.

[Mario Carneiro]

data.nat.cast -> algebra.ne_zero seems super suspicious

[Eric Rodriguez]

I thought I turned that inside out? I'm not sure what happened

[Eric Rodriguez]

maybe it was for add_monoid_with_one stuff

[Eric Rodriguez]

it used to import algebra.invertible before too :)

[Mario Carneiro]

I feel like we need a bot that posts about "dependency regressions" in mathlib similar to performance regressions in software projects. "The average number of transitive dependencies went up by 10 by this PR" would be nice to see

[Ruben Van de Velde]

This seems to compile, fwiw:

--- src/algebra/invertible.lean
+++ src/algebra/invertible.lean
@@ -5,7 +5,8 @@ Authors: Anne Baanen
 -/

 import algebra.group.units
-import algebra.ne_zero
+import algebra.group_with_zero.units
+--import algebra.ne_zero
 import algebra.ring.basic

 /-!
@@ -214,8 +215,8 @@ lemma nonzero_of_invertible [mul_zero_one_class α] (a : α) [nontrivial α] [in
 λ ha, zero_ne_one $ calc   0 = ⅟a * a : by simp [ha]
                          ... = 1 : inv_of_mul_self a

-@[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)
-  [invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩
+--@[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)
+--  [invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩

 section monoid_with_zero
 variable [monoid_with_zero α]

[Eric Wieser]

I think a nicer refactor would be to push ne_zero much lower

[Eric Wieser]

#17171

[Mario Carneiro]

what does leanproject import-graph give you after that PR @Eric Wieser ?

[Scott Morrison]

algebra.invertible.pdf

[Scott Morrison]

So it's a fair improvement (by avoiding data.nat.cast, we transitively avoid data.set.lattice and bunch of its imports).

[Scott Morrison]

But there's still a undigestible bolus of order theory coming in via data.nat.basic

[Mario Carneiro]

algebra.group_power.basic says:

The power operation on monoids and groups.
We separate this from group, because it depends on `ℕ`,
which in turn depends on other parts of algebra.

So it seems like this is expected for group power, but algebra.group_power.ring -> algebra.ne_zero now sounds even more suspicious

[Mario Carneiro]

yep, there is exactly one thing in the file that uses that bolus:

instance pow [monoid_with_zero M] [no_zero_divisors M] [ne_zero x] : ne_zero (x ^ n) :=
⟨pow_ne_zero n out⟩

We can easily invert this dependency.

[Scott Morrison]

#17175

[Scott Morrison]

Hmmm, that still leaves us with algebra.ne_zero importing algebra.order.ring, because of

instance bit1 [canonically_ordered_comm_semiring M] [nontrivial M] : ne_zero (bit1 x) :=
⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) zero_lt_one.not_le⟩

I bet if we can move that as well we can really lower algebra.ne_zero and algebra.invertible.

[Scott Morrison]

#17176

[Scott Morrison]

Ah, nice. The supremum of #17171, #17174, #17175, and #17176 reduces the import hierarchy for algebra.invertible to:
algebra.invertible.sup.pdf, which is much more manageable.

[Scott Morrison]

I bet we could strip even more: surely logic.embedding is not really needed here. But not for now. :-)

[Mario Carneiro]

Well, I did :) #17177

[Mario Carneiro]

algebra.invertible.pdf

[Mario Carneiro]

now that dependency graph actually makes sense

[Scott Morrison]

#17179 will remove a further two nodes from that graph.

[Scott Morrison]

and #17180 another two. :-)

[Ruben Van de Velde]

Mario Carneiro said:

Well, I did :) #17177

Fwiw, you got a "rejected by label" from bors

[Kevin Buzzard]

What's the difference between light blue and dark blue again?

[Yakov Pechersky]

light blue is "all prereqs met", darker blue is "there is PR but it's not merged yet"

[Yakov Pechersky]

More precisely, "ready to start porting, all prereqs present" is turquoise1, "there is an unmerged PR" is lightskyblue

[Kevin Buzzard]

If I turn my data.bool.basic port branch into a PR (I got everything compiling yesterday for the first time, it's also a port of a core Lean file) then how does the system know there's a PR for data.bool.basic?

[Yakov Pechersky]

You have to edit the file here: https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

[Kevin Buzzard]

Got it -- sorry I'm learning a new trick here and it takes time

[Jannis Limperg]

(wrong thread again, why does this only happen to me?)

[Scott Morrison]

An update on porting progress. Here are some graphs for interesting targets:

• algebra.invertible.pdf (post #17177)
• limits.pdf
• algebra.order.ring.pdf

Here's the list of currently available porting targets:

data.fun_like.basic
data.prod.basic    -- WIP
data.subtype
data.option.basic    -- PRd as mathlib4#493
logic.function.conjugate
data.nat.cast.defs
data.bool.basic    -- WIP Kevin Buzzard
logic.relation
control.functor
lean_core.data.vector
data.char
logic.lemmas
algebra.order.floor    -- Blocked by tactic.abel and tactic.linarith

(plus some lower priority stuff). It's tempting to believe that data.fun_like.[basic|embedding|equiv] could possibly be done as a single PR.

[Scott Morrison]

Both abel and linarith have open PRs that more-or-less work, so someone brave could start on algebra.order.floor by merging those branches into theirs.

[Kevin Buzzard]

I've taken a look at data.fun_like.basic and data.subtype and I think they're both beyond my pay grade. data.fun_like.basic assumes more about coercions than I know (but if someone wants to start me off I can have a go) and data.subtype uses stuff like initialize_simps_projections which I don't understand and might not even be ported yet.

[Mario Carneiro]

Could someone move the units section out of data.int.basic? That section requires more imports than everything else.

[Moritz Doll]

Mario are you on a recent branch? data.int.basic has two imports for me: data.nat.basic and order.monotone, the former is obviously necessary and the later is used only for

lemma coe_nat_strict_mono : strict_mono (coe : ℕ → ℤ) := λ _ _, int.coe_nat_lt.2

[Moritz Doll]

and there is a file data.int.units already that imports algebra.group_power.order and lots of other stuff through data.int.order.basic

[Scott Morrison]

This change just landed in the last day or two.

[Mario Carneiro]

Note that I did not judge that by looking at the import line, but rather by the fact that the file is full of stuff that typechecks with almost no imports, and then there is a section at the bottom with a bunch of fancy things from mathlib algebra

[Mario Carneiro]

(I'm actually moving that file to Std so that section sticks out)

[Scott Morrison]

@Moritz Doll, are you still working on this?

[Scott Morrison]

(I'm tempted to have a look at rearranging to remove uses of units, but don't want to duplicate if you're already doing this.)

[Moritz Doll]

I don't really know how to do it properly, so it might be better if you do it

[Scott Morrison]

On it.

[Scott Morrison]

#17508

[Michael Stoll]

Scott Morrison said:

#17508

While you are doing that, can you perhaps include the additional lemmas from #17478 ?

[Scott Morrison]

Could you explain why that's better than two separate PRs?

[Michael Stoll]

Less work? If one gets merged, the other needs to be changed in any case, so why not do it right away? This probably saves some CI cycles, too.

[Scott Morrison]

Hmm... I'm conflicted. I like having the refactoring PRs neither add or remove material, so it's easier to be sure they are only refactors. :-)

[Scott Morrison]

But I do like not having things rot on the queue!

[Michael Stoll]

OK; I'll leave it to you to resolve this conflict :smile:.

[Eric Wieser]

I've sent #17478 to bors

[Eric Wieser]

Oh, I now see that the other one is also on the queue

[Eric Wieser]

I guess I'll let bors decide which one to spit out (or @Scott Morrison if you get there first)

[Michael Stoll]

They are in the same batch, so this batch will fail.

[Eric Wieser]

Bors will split the batch automatically if the merge conflicts

[Michael Stoll]

Looks like mine will get there first...

[Eric Rodriguez]

there's no real porting targets that seem open and mathematical right now, so what other tasks are there for someone wanting to get involved?

[Eric Rodriguez]

image.png for this section, is it about just eyeballing the files and making sure there's no big changes?

[Heather Macbeth]

After #17616 lands, I think it would be useful to do a similar task for data.list.big_operators. That file has a lot of imports. It lies on the path to data.list.perm and through that to data.fintype.basic, so anything you could strip from that path would be helpful.

[Heather Macbeth]

Or maybe we don't need big operators for the part of data.list.perm needed for fintype? So maybe the split should happen higher up? Anyway, I'm not sure, but it's worth looking into.

[Heather Macbeth]

It just doesn't seem like we should need lemmas about divisibility to define fintype ....

[Jireh Loreaux]

About the "the following files have been modified since the commit ...."

Two things:

1. I think the plan is to at some point have a flag for the port_status script which will help you do this, but for now ...
2. Take the file in question and git diff port-status-SHA master -- /path/to/file (in mathlib3). If the only change is the mathlib4 synchronization label, then update the port-status page for the file with the current SHA from mathlib master.

If there are new changes to the file, then port the new changes to mathlib4 (or make sure they are already there somehow).

[Patrick Massot]

Eric Rodriguez said:

there's no real porting targets that seem open and mathematical right now, so what other tasks are there for someone wanting to get involved?

Porting targets that are not mathematical.

[Jireh Loreaux]

To second Patrick's point, you are likely capable of porting the non-mathematical things, e.g., I doubt data.stream.defs would be that hard, but I haven't looked carefully.

[Arien Malec]

I’ve been following a heuristic of “not deeply mathematical” and ideally non-critical path & if I can do some grunt work that helps more experienced folks hone in on the hard bits that’s fine too. Helps to have a generally high tolerance for grunt work or wasted effort if it helps expose issues (see my many adventures discovering things already in Std or only on critical path for tactics)

[Eric Rodriguez]

I felt less confident about them because I'm more likely to mess up important meta-details; I'll still give it a shot, though

[Arien Malec]

I prefer to change little, not make any change that I don’t understand, and comment on any uncertainty….

[Eric Rodriguez]

Jireh Loreaux said:

About the "the following files have been modified since the commit ...."

Two things:

1. I think the plan is to at some point have a flag for the port_status script which will help you do this, but for now ...
2. Take the file in question and git diff port-status-SHA master -- /path/to/file (in mathlib3). If the only change is the mathlib4 synchronization label, then update the port-status page for the file with the current SHA from mathlib master.

If there are new changes to the file, then port the new changes to mathlib4 (or make sure they are already there somehow).

I've just made #17630, which adds a simple option that outputs the required git diff command. Hopefully it makes it less work to check this.

[Eric Rodriguez]

using this script patch, I very coarsely verified that the following files are ported okay (I excluded any files that had even a non-trivial import change for quick checking):

order.synonym
order.compare
order.monotone
order.max
order.rel_classes
category_theory.concrete_category.bundled
logic.pairwise
logic.nonempty
logic.unique
logic.relation
logic.is_empty
logic.relator
logic.equiv.defs
logic.function.iterate
logic.function.conjugate
data.subtype
data.quot
data.bracket
data.char
data.prod.pprod
data.fun_like.embedding
data.fun_like.equiv
data.fin.fin2
data.num.basic
data.option.defs
data.pnat.defs
algebra.abs
algebra.covariant_and_contravariant
algebra.order.ring.lemmas
algebra.group.commutator
algebra.group_power.identities
algebra.homology.complex_shape

If anyone else can verify these, I'll change these's SHAs on the status page

[Eric Rodriguez]

(a helpful git option was git config pager.diff false

[Jireh Loreaux]

Note: your script should diff against master, not HEAD

[Jireh Loreaux]

Just in case someone is on another branch without realizing it.

[Eric Rodriguez]

Do you think I should make that change generally to the script or just when outputting? I wonder if this current functionality is useful for someone preparing a PR to do with mathlib4

[Eric Rodriguez]

Jireh Loreaux said:

To second Patrick's point, you are likely capable of porting the non-mathematical things, e.g., I doubt data.stream.defs would be that hard, but I haven't looked carefully.

oh, there's another definition of Stream already

[Jireh Loreaux]

I ran all the diffs against c4658a649d216f57e99621708b09dcb3dcccbd23 on master. Looks like data.bool.basic can also go on your list. However, I think the following fileshave changes (and I have not checked them against mathlib4). If you checked them against mathlib4, that's fine, but if you haven't don't update the SHAs.

• order.compare
• category_theory.concrete_category.bundled
• logic.equiv.defs
• data.subtype
• data.fun_like.equiv

[Jireh Loreaux]

If you have time and are willing, you could synchronize the files that need it with mathlib4, but I don't have time tonight to try and do that.

[Eric Rodriguez]

Okay, I checked most of those manually as well (just proof changes apart from fun_like.equiv). I'll put these in and maybe I'll fix discrepancies on others later

[Scott Morrison]

Looking at the state of things this morning, the really really helpful thing that people can do is review each others PRs (e.g. check #align's, fix errors, mark as approved), and then post in a thread here requests for merging (or merge yourself if you self-identify as someone who should do that :-)

[Scott Morrison]

We have a big PR queue.

[Scott Morrison]

If someone could add the #queue4 linkifier that would be lovely.

[Scott Morrison]

Oh! It exists. :-)

[Scott Morrison]

Okay --- go forth and review all those PRs, and anything that looks ready to go, hunt down someone who will hit bors merge on it. :-)

[Scott Morrison]

I am soon to be essentially offline for 72 hours, due to some complicated travel.

[Scott Morrison]

Priorities for attention should be #641 and #631.

[Eric Rodriguez]

mathlib4#641, mathlib4#631

[Eric Rodriguez]

Is there any chance we could ask people to in future just commit the raw mathbin file as the first commit?

[Scott Morrison]

Yes! It's been suggested before. @Eric Rodriguez, would you verify that it is in the wiki?

[Eric Rodriguez]

No, it hasn't. I'll add it now

[Scott Morrison]

In fact, I'd say mathlib4#641 is ready to go, except for the library_note "coercion into rings" needing updating.

[Scott Morrison]

If @Gabriel Ebner would be willing to either rewrite that, or just say "please leave a 'Porting note' that this library note is out of date and needs repair", then I think we should merge.

[Gabriel Ebner]

Okay I've rewrote the library note.

[Scott Morrison]

Haha, great, the solution was to delete the confusing paragraph. :-)

[Arien Malec]

I believe mathlib4#616 and mathlib4#649 are good to go pending review. mathlib4#638 has a universe linting error if good just needs an override.

[Jireh Loreaux]

Probably you should fix the universe linting error. Let me know if you need help.

[Arien Malec]

I definitely need help -- not sure what's causing it...

[Jireh Loreaux]

I'll try to have a quick look in an hour or so.

[Arien Malec]

The reason I think this is OK is that it occurs in the typeclass instances for ULift which is designed to do universe shenanigans. In particular, the lint is for "max u v in the type where neither u nor v occur by themselves" but ULift by definition maps to Type (max s r)

[Mario Carneiro]

The lint is for when u and v appear together as max u v everywhere in the declaration and proof. If you use ULift.{u, v} then u and v are appearing separately

[Arien Malec]

The code is never using max u v; this only happens behind the scenes in the typeclass instance. It's possible I need a fix by adding explicit universe types for all the invocations of ULift?

[Mario Carneiro]

I mean the elaborated term uses max u v

[Mario Carneiro]

(If you have a specific example in mind you should probably do it on another thread, this one is about porting requests and progress toward them)

[Casavaca]

I just picked up a light blue node and ported it. Is this change desired? https://github.com/leanprover-community/mathlib4/pull/1307 Port/order.concept

[Casavaca]

Anyone interested to help me with this pull request?

[Kevin Buzzard]

Usually pull requests are made from branches of leanprover-community/mathlib4 ; I'm not sure your PR will ever make it onto #queue4 because it hasn't been done in this way. Why not ping the maintainers letting them now your github userid and ask for push access to non-master branches of mathlib4? I don't ever look at the PRs in mathlib4, I only ever look at #queue4 because those are the PRs which are "ready for review".

[Casavaca]

That's helpful. Thanks.

[Kevin Buzzard]

PS I also looked at your PR today given that you flagged it explicitly :-)